文章基本信息
- 标题：Representing Isabelle in LF
- 本地全文：下载
- 作者：Florian Rabe
- 期刊名称：Electronic Proceedings in Theoretical Computer Science
- 电子版ISSN：2075-2180
- 出版年度：2010
- 卷号：34
- 页码：85-99
- DOI：10.4204/EPTCS.34.8
- 出版社：Open Publishing Association
- 摘要：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.
