Modular Monadic Meta-Theory [pdf] [bib]

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 individual 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{3mt,
  author =       "Delaware, Benjamin and Keuchel, Steven and
                  Schrijvers, Tom and Oliveira, Bruno C. d. S.",
  title =        "{M}odular {M}onadic {M}eta-{T}heory",
  booktitle =    "Proceedings of the 18th ACM SIGPLAN international 
                  conference on Functional programming",
  series =       "ICFP '13",
  year =         "2013",
  numpages =     "12",
  doi =          "10.1145/2500365.2500587",
  publisher =    "ACM",
  note =         "Boston, Massachusetts, USA, September 25--27, 2013"
}

Submission Annex

The developments of this paper can be found in this GitHub repository.