A Practical Module System for LF

Carsten Schürmann, Florian Rabe

    Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer 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.
    OriginalsprogEngelsk
    TitelProceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
    Antal sider48
    ForlagAssociation for Computing Machinery
    Publikationsdato2009
    Sider40
    ISBN (Trykt)978-1-60558-529-1
    StatusUdgivet - 2009
    BegivenhedFourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - Montreal, Canada
    Varighed: 2 aug. 20092 aug. 2009
    Konferencens nummer: 4

    Konference

    KonferenceFourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
    Nummer4
    Land/OmrådeCanada
    ByMontreal
    Periode02/08/200902/08/2009

    Emneord

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

    Citationsformater