A Practical Module System for LF

Carsten Schürmann; Florian Rabe

A Practical Module System for LF

Constructor University

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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.

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

Citationsformater

@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 -