Representing Isabelle in LF

TL;DR

This paper presents a novel method for representing the Isabelle logical framework within LF, incorporating advanced features like type classes and locales through an extended module system.

Contribution

It introduces a new representation of Isabelle in LF that includes morphism variables and abstractions, extending the LF module system to support these features.

Findings

Successfully represented Isabelle features like type classes and locales in LF.

Extended the LF module system to include morphism variables and abstraction.

Maintained conservativeness in expressivity while enhancing modularity.

Abstract

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.