File Download

There are no files associated with this item.

  Links for fulltext
     (May Require Subscription)
Supplementary

Conference Paper: Meta-theory à la Carte

TitleMeta-theory à la Carte
Authors
KeywordsCoq
Extensible Church Encodings
Modular Mechanized Meta-Theory
Issue Date2013
Citation
Acm Sigplan Notices, 2013, v. 48 n. 1, p. 207-218 How to Cite?
AbstractFormalizing meta-theory, or proofs about programming languages, in a proof assistant has many well-known benefits. Unfortunately, the considerable effort involved in mechanizing proofs has prevented it from becoming standard practice. This cost can be amortized by reusing as much of existing mechanized formalizations as possible when building a new language or extending an existing one. One important challenge in achieving reuse is that the inductive definitions and proofs used in these formalizations are closed to extension. This forces language designers to cut and paste existing definitions and proofs in an ad-hoc manner and to expend considerable effort to patch up the results. The key contribution of this paper is the development of an induction technique for extensible Church encodings using a novel reinterpretation of the universal property of folds. These encodings provide the foundation for a framework, formalized in Coq, which uses type classes to automate the composition of proofs from modular components. This framework enables a more structured approach to the reuse of meta-theory formalizations through the composition of modular inductive definitions and proofs. Several interesting language features, including binders and general recursion, illustrate the capabilities of our framework. We reuse these features to build fully mechanized definitions and proofs for a number of languages, including a version of mini-ML. Bounded induction enables proofs of properties for non-inductive semantic functions, and mediating type classes enable proof adaptation for more feature-rich languages. Copyright © 2013 ACM.
Persistent Identifierhttp://hdl.handle.net/10722/188507
ISSN
2015 SCImago Journal Rankings: 0.490
ISI Accession Number ID
References

 

DC FieldValueLanguage
dc.contributor.authorDelaware, Ben_US
dc.contributor.authorOliveira, BCDSen_US
dc.contributor.authorSchrijvers, Ten_US
dc.date.accessioned2013-09-03T04:08:47Z-
dc.date.available2013-09-03T04:08:47Z-
dc.date.issued2013en_US
dc.identifier.citationAcm Sigplan Notices, 2013, v. 48 n. 1, p. 207-218en_US
dc.identifier.issn1523-2867en_US
dc.identifier.urihttp://hdl.handle.net/10722/188507-
dc.description.abstractFormalizing meta-theory, or proofs about programming languages, in a proof assistant has many well-known benefits. Unfortunately, the considerable effort involved in mechanizing proofs has prevented it from becoming standard practice. This cost can be amortized by reusing as much of existing mechanized formalizations as possible when building a new language or extending an existing one. One important challenge in achieving reuse is that the inductive definitions and proofs used in these formalizations are closed to extension. This forces language designers to cut and paste existing definitions and proofs in an ad-hoc manner and to expend considerable effort to patch up the results. The key contribution of this paper is the development of an induction technique for extensible Church encodings using a novel reinterpretation of the universal property of folds. These encodings provide the foundation for a framework, formalized in Coq, which uses type classes to automate the composition of proofs from modular components. This framework enables a more structured approach to the reuse of meta-theory formalizations through the composition of modular inductive definitions and proofs. Several interesting language features, including binders and general recursion, illustrate the capabilities of our framework. We reuse these features to build fully mechanized definitions and proofs for a number of languages, including a version of mini-ML. Bounded induction enables proofs of properties for non-inductive semantic functions, and mediating type classes enable proof adaptation for more feature-rich languages. Copyright © 2013 ACM.en_US
dc.languageengen_US
dc.relation.ispartofACM SIGPLAN Noticesen_US
dc.subjectCoqen_US
dc.subjectExtensible Church Encodingsen_US
dc.subjectModular Mechanized Meta-Theoryen_US
dc.titleMeta-theory à la Carteen_US
dc.typeConference_Paperen_US
dc.identifier.emailOliveira, BCDS: oliveira@comp.nus.edu.sgen_US
dc.identifier.authorityOliveira, BCDS=rp01786en_US
dc.description.naturelink_to_subscribed_fulltexten_US
dc.identifier.doi10.1145/2480359.2429094en_US
dc.identifier.scopuseid_2-s2.0-84877897023en_US
dc.relation.referenceshttp://www.scopus.com/mlt/select.url?eid=2-s2.0-84877897023&selection=ref&src=s&origin=recordpageen_US
dc.identifier.volume48en_US
dc.identifier.issue1en_US
dc.identifier.spage207en_US
dc.identifier.epage218en_US
dc.identifier.isiWOS:000318629900018-
dc.publisher.placeUnited Statesen_US
dc.identifier.scopusauthoridDelaware, B=35742891200en_US
dc.identifier.scopusauthoridOliveira, BCDS=12239474400en_US
dc.identifier.scopusauthoridSchrijvers, T=8870481000en_US

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats