A Practical Module System for LF

Carsten Schürmann, Florian Rabe

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

    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 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
    EventFourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - Montreal, Canada
    Duration: 2 Aug 20092 Aug 2009
    Conference number: 4

    Conference

    ConferenceFourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
    Number4
    Country/TerritoryCanada
    CityMontreal
    Period02/08/200902/08/2009

    Keywords

    • Module Systems
    • Logical Framework
    • Signature Morphisms
    • Meta-theory Mechanization
    • Twelf Implementation

    Cite this