Representing Isabelle in LF

Florian Rabe
(Jacobs University Bremen)

LF has been designed and successfully used as a meta-logical framework to represent and reason about object logics. Here we design a representation of the Isabelle logical framework in LF using the recently introduced module system for LF. The major novelty of our approach is that we can naturally represent the advanced Isabelle features of type classes and locales.

Our representation of type classes relies on a feature so far lacking in the LF module system: morphism variables and abstraction over them. While conservative over the present system in terms of expressivity, this feature is needed for a representation of type classes that preserves the modular structure. Therefore, we also design the necessary extension of the LF module system.

In Karl Crary and Marino Miculan: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2010), Edinburgh, UK, 14th July 2010, Electronic Proceedings in Theoretical Computer Science 34, pp. 85–99.
Published: 11th September 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.34.8 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org