Title: Meta-Theory a la Carte
Authors: Delaware, Benjamin ×
Oliveira, Bruno C. D. S
Schrijvers, Tom #
Issue Date: 2013
Publisher: ACM Press
Series Title: ACM SIGPLAN Notices vol:48 issue:1 pages:207-218
Abstract: Formalizing meta-theory, or proofs about programming languages, in a
proof assistant has many well-known benefits. However, the considerable effort
involved in mechanizing proofs has prevented it from becoming standard
practice. This cost can be amortized by reusing as much of
an existing formalization as possible when building a new language or
extending an existing one. Unfortunately reuse of components is
typically ad-hoc, with the language designer cutting and pasting
existing definitions and proofs, and expending considerable effort to
patch up the results.

This paper presents a more structured approach to the reuse of
formalizations of programming language semantics through the
composition of modular definitions and proofs. The key contribution
is the development of an approach to induction for extensible Church
encodings which uses a novel reinterpretation of the universal
property of folds. These encodings provide the foundation for a
framework, formalized in Coq, which uses type classes to automate the
composition of proofs from modular components.

Several interesting language features, including binders and general
recursion, illustrate the capabilities of our framework. We reuse
these features to build fully mechanized definitions and proofs for a
number of languages, including a version of mini-ML. Bounded induction
enables proofs of properties for non-inductive semantic functions, and
mediating type classes enable proof adaptation for more feature-rich
ISSN: 0362-1340
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Non-KU Leuven Association publications
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
popl2013.pdfarticle Published 219KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science