Abstract
Module Systems for proof assistants provide administrative support for large developments when mechanizing the meta-theory of programming languages and logics. In this paper we describe a module system for the logical framework LF. It is based on two main primitives: signatures and signature morphisms, which provide a semantically transparent module level and permit to represent logic translations as homomorphisms. Modular LF is a conser- vative extension over LF, and integrates an elaboration of modular into core LF signatures. We have implemented our design in the Twelf system and used it to modularize large parts of the Twelf example library.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice |
| Number of pages | 48 |
| Publisher | Association for Computing Machinery |
| Publication date | 2009 |
| Pages | 40 |
| ISBN (Print) | 978-1-60558-529-1 |
| Publication status | Published - 2009 |
| Event | Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - Montreal, Canada Duration: 2 Aug 2009 → 2 Aug 2009 Conference number: 4 |
Conference
| Conference | Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice |
|---|---|
| Number | 4 |
| Country/Territory | Canada |
| City | Montreal |
| Period | 02/08/2009 → 02/08/2009 |
Keywords
- Module Systems
- Logical Framework
- Signature Morphisms
- Meta-theory Mechanization
- Twelf Implementation