File Download
There are no files associated with this item.
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.1145/2500365.2500587
- Scopus: eid_2-s2.0-84887164591
- WOS: WOS:000327696700030
Supplementary
- Citations:
- Appears in Collections:
Conference Paper: Modular Monadic Meta-Theory
Title | Modular Monadic Meta-Theory |
---|---|
Authors | |
Keywords | Mechanized meta-theory Modularity Monads Side-effects |
Issue Date | 2013 |
Publisher | The Association for Computing Machinery (ACM). |
Citation | Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (ICFP 2013): Boston, Massachusetts, USA, 25-27 September 2013, p. 319-330 How to Cite? |
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. |
Description | Session 11: Modular Meta-Theory |
Persistent Identifier | http://hdl.handle.net/10722/203652 |
ISBN | |
ISI Accession Number ID |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Delaware, B | en_US |
dc.contributor.author | Keuchel, S | en_US |
dc.contributor.author | Schrijvers, T | en_US |
dc.contributor.author | dos Santos Oliveira, BC | en_US |
dc.date.accessioned | 2014-09-19T15:49:10Z | - |
dc.date.available | 2014-09-19T15:49:10Z | - |
dc.date.issued | 2013 | en_US |
dc.identifier.citation | Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (ICFP 2013): Boston, Massachusetts, USA, 25-27 September 2013, p. 319-330 | en_US |
dc.identifier.isbn | 9781450323260 | - |
dc.identifier.uri | http://hdl.handle.net/10722/203652 | - |
dc.description | Session 11: Modular Meta-Theory | - |
dc.description.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. | en_US |
dc.language | eng | en_US |
dc.publisher | The Association for Computing Machinery (ACM). | en_US |
dc.relation.ispartof | Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (ICFP 2013) | en_US |
dc.subject | Mechanized meta-theory | - |
dc.subject | Modularity | - |
dc.subject | Monads | - |
dc.subject | Side-effects | - |
dc.title | Modular Monadic Meta-Theory | en_US |
dc.type | Conference_Paper | en_US |
dc.identifier.email | dos Santos Oliveira, BC: bruno@hku.hk | en_US |
dc.identifier.authority | dos Santos Oliveira, BC=rp01786 | en_US |
dc.identifier.doi | 10.1145/2500365.2500587 | en_US |
dc.identifier.scopus | eid_2-s2.0-84887164591 | - |
dc.identifier.hkuros | 239761 | en_US |
dc.identifier.spage | 319 | en_US |
dc.identifier.epage | 330 | en_US |
dc.identifier.isi | WOS:000327696700030 | - |
dc.publisher.place | New York | en_US |