Sorry for the long delay in posting any updates. This last week, I was invited to give a talk in Sussex on name binding. In my talk, I was discussing some of the problems with (“strong”) HOAS, specifically negative occurences in the types of constructors, and the problems with using these in Coq. An audience member asked where he could read more about this problem, and ways around it. As I’ve already posted the two papers I suggested, I’ll add a third:
By Venanzio Capretta and Amy P. Felty, from TYPES 2006, available from Amy P. Felty’s website:
The use of higher-order abstract syntax is an important approach for the representation of binding constructs in encodings of languages and logics in a logical framework. Formal meta-reasoning about such object languages is a particular challenge. We present a mechanism for such reasoning, formalized in Coq, inspired by the Hybrid tool in Isabelle. At the base level, we define a de Bruijn representation of terms with basic operations and a reasoning framework. At a higher level, we can represent languages and reason about them using higher-order syntax. We take advantage of Coq’s constructive logic by formulating many definitions as Coq programs. We illustrate the method on two examples: the untyped lambda calculus and quantified propositional logic. For each language, we can define recursion and induction principles that work directly on the higher-order syntax.
Coq source files are available here.