This 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
CITATION STYLE
Lee, G., Oliveira, B. C. D. S., Cho, S., & Yi, K. (2012). GMeta: A generic formal metatheory framework for first-order representations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7211 LNCS, pp. 436–455). https://doi.org/10.1007/978-3-642-28869-2_22
Mendeley helps you to discover research relevant for your work.