Notice

The website of Tom Schrijvers has moved to http://people.cs.kuleuven.be/~tom.schrijvers. Please adjust any links you maintain as this copy will be taken down shortly.


Modular Monadic Meta-Theory


Benjamin Delaware and Steven Keuchel en Tom Schrijvers and Bruno C. d. S. Oliveira.
International Conference on Functional Programming (ICFP).
Tarmo Uustalu, eds.
2013.

Abstract

This paper presents 3MT, a framework for modular mechanized meta-theory of languages with effects. Using 3MT, individual language features and their corresponding definitions -- semantic functions, theorem statements and proofs -- can be built separately and then reused to create different languages with fully mechanized meta-theory. 3MT combines modular datatypes and monads to define denotational semantics with effects on a per-feature basis, without fixing the particular set of effects or language constructs. One well-established problem with type soundness proofs for denotational semantics is that they are notoriously brittle with respect to the addition of new effects. The statement of type soundness for a language depends intimately on the effects it uses, making it particularly challenging to achieve modularity. 3MT solves this long-standing problem by splitting these theorems into two separate and reusable parts: a feature theorem that captures the well-typing of denotations produced by the semantic function of an invidual feature with respect to only the effects used, and an effect theorem that adapts well-typings of denotations to a fixed superset of effects. The proof of type soundness for a particular language simply combines these theorems for its features and the combination of their effects. To establish both theorems, 3MT uses two key reasoning techniques: modular induction and algebraic laws about effects. Several effectful language features, including references and errors, illustrate the capabilities of 3MT. A case study reuses these features to build fully mechanized definitions and proofs for 28 languages, including several versions of mini-ML with effects.

BibTeX

@inproceedings{icfp2013,
  author = {Benjamin Delaware and Steven Keuchel en Tom Schrijvers and Bruno C. d. S. Oliveira},
  editor = {Tarmo Uustalu},
  title = {Modular Monadic Meta-Theory},
  booktitle = {International Conference on Functional Programming (ICFP)},
  url = {/Research/papers/icfp2013.pdf},
  year = {2013},
  abstract = {This paper presents 3MT, a framework for modular
mechanized meta-theory of languages with effects. Using 3MT,
individual language features and their corresponding definitions --
semantic functions, theorem statements and proofs
-- can be built separately and then reused to create different
languages with fully mechanized meta-theory.  3MT combines
modular datatypes and monads to define
denotational semantics with effects on a per-feature basis, without fixing the
particular set of effects or language constructs.

One well-established problem with type soundness proofs for
denotational semantics is that they are notoriously brittle with
respect to the addition of new effects.
The statement of type soundness for a language depends intimately on the
effects it uses, making it particularly
challenging to achieve modularity. 3MT solves this long-standing problem by splitting these theorems into
two separate and reusable parts: a feature theorem that captures
the well-typing of denotations
produced by the semantic function of an invidual feature with respect
to only the effects used,
and an effect theorem that adapts well-typings of denotations to a
fixed superset of effects.
The proof of type soundness for a particular language simply combines these theorems for its features
and the combination of their effects.
To establish both theorems, 3MT uses two key reasoning techniques:
modular induction and algebraic laws about effects. Several
effectful language features, including references and errors, illustrate the
capabilities of 3MT. A case study reuses these features to build fully
mechanized definitions and proofs for 28 languages, including several
versions of mini-ML with effects.
},
}