A Practical Module System for LF

Carsten Schürmann; Florian Rabe

A Practical Module System for LF

Constructor University

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-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 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

Cite this

@inproceedings{e10de990e31411dea523000ea68e967b,

title = "A Practical Module System for LF",

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.",

keywords = "Module Systems, Logical Framework, Signature Morphisms, Meta-theory Mechanization, Twelf Implementation, Module Systems, Logical Framework, Signature Morphisms, Meta-theory Mechanization, Twelf Implementation",

author = "Carsten Sch{\"u}rmann and Florian Rabe",

year = "2009",

language = "English",

isbn = "978-1-60558-529-1",

pages = "40",

booktitle = "Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice",

publisher = "Association for Computing Machinery",

address = "United States",

note = "Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice ; Conference date: 02-08-2009 Through 02-08-2009",

}

TY - GEN

T1 - A Practical Module System for LF

AU - Schürmann, Carsten

AU - Rabe, Florian

N1 - Conference code: 4

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

KW - Module Systems

KW - Logical Framework

KW - Signature Morphisms

KW - Meta-theory Mechanization

KW - Twelf Implementation

KW - Module Systems

KW - Logical Framework

KW - Signature Morphisms

KW - Meta-theory Mechanization

KW - Twelf Implementation

M3 - Article in proceedings

SN - 978-1-60558-529-1

SP - 40

BT - Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice

PB - Association for Computing Machinery

T2 - Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice

Y2 - 2 August 2009 through 2 August 2009

ER -