Dictionary Construction

Lars Hupel 🌐

May 24, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

Isabelle's code generator natively supports type classes. For targets that do not have language support for classes and instances, it performs the well-known dictionary translation, as described by Haftmann and Nipkow. This translation happens outside the logic, i.e., there is no guarantee that it is correct, besides the pen-and-paper proof. This work implements a certified dictionary translation that produces new class-free constants and derives equality theorems.

License

BSD License

Topics

Session Dict_Construction