File Download

There are no files associated with this item.

  Links for fulltext
     (May Require Subscription)
Supplementary

Conference Paper: GMeta: A generic formal metatheory framework for first-order representations

TitleGMeta: A generic formal metatheory framework for first-order representations
Authors
KeywordsCoq
Datatype-Generic Programming
First-Order Representations
Mechanization
Poplmark Challenge
Variable Binding
Issue Date2012
PublisherSpringer Verlag. The Journal's web site is located at http://springerlink.com/content/105633/
Citation
Lecture Notes In Computer Science (Including Subseries Lecture Notes In Artificial Intelligence And Lecture Notes In Bioinformatics), 2012, v. 7211 LNCS, p. 436-455 How to Cite?
AbstractThis paper presents GMeta: a generic framework for first-order representations of variable binding that provides once and for all many of the so-called infrastructure lemmas and definitions required in mechanizations of formal metatheory. The key idea is to employ datatype-generic programming (DGP) and modular programming techniques to deal with the infrastructure overhead. Using a generic universe for representing a large family of object languages we define datatype-generic libraries of infrastructure for first-order representations such as locally nameless or de Bruijn indices. Modules are used to provide templates: a convenient interface between the datatype-generic libraries and the end-users of GMeta. We conducted case studies based on the POPLmark challenge, and showed that dealing with challenging binding constructs, like the ones found in System F <:, is possible with GMeta. All of GMeta's generic infrastructure is implemented in the Coq theorem prover. Furthermore, due to GMeta's modular design, the libraries can be easily used, extended, and customized by users. © 2012 Springer-Verlag.
Persistent Identifierhttp://hdl.handle.net/10722/188496
ISSN
2005 Impact Factor: 0.402
2015 SCImago Journal Rankings: 0.252
References

 

DC FieldValueLanguage
dc.contributor.authorLee, Gen_US
dc.contributor.authorOliveira, BCDSen_US
dc.contributor.authorCho, Sen_US
dc.contributor.authorYi, Ken_US
dc.date.accessioned2013-09-03T04:08:44Z-
dc.date.available2013-09-03T04:08:44Z-
dc.date.issued2012en_US
dc.identifier.citationLecture Notes In Computer Science (Including Subseries Lecture Notes In Artificial Intelligence And Lecture Notes In Bioinformatics), 2012, v. 7211 LNCS, p. 436-455en_US
dc.identifier.issn0302-9743en_US
dc.identifier.urihttp://hdl.handle.net/10722/188496-
dc.description.abstractThis paper presents GMeta: a generic framework for first-order representations of variable binding that provides once and for all many of the so-called infrastructure lemmas and definitions required in mechanizations of formal metatheory. The key idea is to employ datatype-generic programming (DGP) and modular programming techniques to deal with the infrastructure overhead. Using a generic universe for representing a large family of object languages we define datatype-generic libraries of infrastructure for first-order representations such as locally nameless or de Bruijn indices. Modules are used to provide templates: a convenient interface between the datatype-generic libraries and the end-users of GMeta. We conducted case studies based on the POPLmark challenge, and showed that dealing with challenging binding constructs, like the ones found in System F <:, is possible with GMeta. All of GMeta's generic infrastructure is implemented in the Coq theorem prover. Furthermore, due to GMeta's modular design, the libraries can be easily used, extended, and customized by users. © 2012 Springer-Verlag.en_US
dc.languageengen_US
dc.publisherSpringer Verlag. The Journal's web site is located at http://springerlink.com/content/105633/en_US
dc.relation.ispartofLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)en_US
dc.subjectCoqen_US
dc.subjectDatatype-Generic Programmingen_US
dc.subjectFirst-Order Representationsen_US
dc.subjectMechanizationen_US
dc.subjectPoplmark Challengeen_US
dc.subjectVariable Bindingen_US
dc.titleGMeta: A generic formal metatheory framework for first-order representationsen_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.1007/978-3-642-28869-2_22en_US
dc.identifier.scopuseid_2-s2.0-84859123251en_US
dc.relation.referenceshttp://www.scopus.com/mlt/select.url?eid=2-s2.0-84859123251&selection=ref&src=s&origin=recordpageen_US
dc.identifier.volume7211 LNCSen_US
dc.identifier.spage436en_US
dc.identifier.epage455en_US
dc.publisher.placeGermanyen_US
dc.identifier.scopusauthoridLee, G=16318940600en_US
dc.identifier.scopusauthoridOliveira, BCDS=12239474400en_US
dc.identifier.scopusauthoridCho, S=55153667400en_US
dc.identifier.scopusauthoridYi, K=7102677014en_US

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats