File Download

There are no files associated with this item.

  Links for fulltext
     (May Require Subscription)
Supplementary

Conference Paper: Modular Monadic Meta-Theory

TitleModular Monadic Meta-Theory
Authors
Issue Date2013
PublisherThe 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?
AbstractThis 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.
DescriptionSession 11: Modular Meta-Theory
Persistent Identifierhttp://hdl.handle.net/10722/203652
ISBN
ISI Accession Number ID

 

DC FieldValueLanguage
dc.contributor.authorDelaware, Ben_US
dc.contributor.authorKeuchel, Sen_US
dc.contributor.authorSchrijvers, Ten_US
dc.contributor.authordos Santos Oliveira, BCen_US
dc.date.accessioned2014-09-19T15:49:10Z-
dc.date.available2014-09-19T15:49:10Z-
dc.date.issued2013en_US
dc.identifier.citationProceedings of the 18th ACM SIGPLAN international conference on Functional programming (ICFP 2013): Boston, Massachusetts, USA, 25-27 September 2013, p. 319-330en_US
dc.identifier.isbn9781450323260-
dc.identifier.urihttp://hdl.handle.net/10722/203652-
dc.descriptionSession 11: Modular Meta-Theory-
dc.description.abstractThis 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.languageengen_US
dc.publisherThe Association for Computing Machinery (ACM).en_US
dc.relation.ispartofProceedings of the 18th ACM SIGPLAN international conference on Functional programming (ICFP 2013)en_US
dc.titleModular Monadic Meta-Theoryen_US
dc.typeConference_Paperen_US
dc.identifier.emaildos Santos Oliveira, BC: bruno@hku.hken_US
dc.identifier.authoritydos Santos Oliveira, BC=rp01786en_US
dc.identifier.doi10.1145/2500365.2500587en_US
dc.identifier.hkuros239761en_US
dc.identifier.spage319en_US
dc.identifier.epage330en_US
dc.identifier.isiWOS:000327696700030-
dc.publisher.placeNew Yorken_US

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats