GMeta: A Generic Formal Metatheory Framework for First-Order Representations

Abstract. This paper presents GMeta: a generic framework for firstorder 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 datatypegeneric 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 endusers 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. Furtherm...

• Type: Journal
• Year: 2012
• Where: ESOP
• Authors: Gyesik Lee, Bruno C. D. S. Oliveira, Sungkeun Cho, Kwangkeun Yi
• Keywords: ESOP 2012, Generic Libraries, Object Languages, Programming Languages, Variable Binding