ITU

A Practical Module System for LF

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

View graph of relations

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 languageEnglish
Title of host publicationProceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Number of pages48
PublisherAssociation for Computing Machinery
Publication date2009
Pages40
ISBN (Print)978-1-60558-529-1
Publication statusPublished - 2009
Event Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - Montreal, Canada
Duration: 2 Aug 20092 Aug 2009
Conference number: 4

Conference

Conference Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Nummer4
LandCanada
ByMontreal
Periode02/08/200902/08/2009

ID: 1036837