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.
| Originalsprog | Engelsk |
|---|---|
| Titel | Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice |
| Antal sider | 48 |
| Forlag | Association for Computing Machinery |
| Publikationsdato | 2009 |
| Sider | 40 |
| ISBN (Trykt) | 978-1-60558-529-1 |
| Status | Udgivet - 2009 |
| Begivenhed | Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - Montreal, Canada Varighed: 2 aug. 2009 → 2 aug. 2009 Konferencens nummer: 4 |
Konference
| Konference | Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice |
|---|---|
| Nummer | 4 |
| Land/Område | Canada |
| By | Montreal |
| Periode | 02/08/2009 → 02/08/2009 |
Emneord
- Module Systems
- Logical Framework
- Signature Morphisms
- Meta-theory Mechanization
- Twelf Implementation