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.

Benjamin Delaware and Steven Keuchel en Tom Schrijvers and Bruno C. d. S. Oliveira.

International Conference on Functional Programming (ICFP).

Tarmo Uustalu, eds.

2013.

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.

@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. }, }