Nominal Reasoning Techniques in Coq (Work in Progress). Brian Aydemir, Aaron Bohannon, and Stephanie Weirich. In International Workshop on Logical Frameworks and Meta-Languages:Theory and Practice (LFMTP 2006).

  We explore an axiomatized nominal approach to variable binding in Coq, using an untyped lambda-calculus as our test case.  In our nominal  approach, alpha-equality of lambda terms coincides with Coq's built-in equality.  Our axiomatization includes a nominal induction principle and functions for calculating free variables and substitution.  These axioms are collected in a module signature and proved sound using locally nameless terms as the underlying representation.  Our experience so far suggests that it is feasible to work from such axiomatized theories in Coq and that the nominal style of variable binding corresponds closely with paper proofs.  We are currently working on proving the soundness of a primitive recursion combinator and developing a method of generating these axioms and their proof of soundness from a grammar describing the syntax of terms and binding.    

[full paper (pdf)] [slides (pdf)] [source code (tar.gz)] [source documentation]

The source code requires Coq 8.1beta to compile. The included README file details differences between the code and the description in the paper.

@InProceedings{aydemir+:nominal-coq,
  author =      {Brian Aydemir and Aaron Bohannon and Stephanie Weirich},
  title =       {Nominal Reasoning Techniques in {Coq}},
  booktitle =   {International Workshop on Logical Frameworks and 
                  Meta-Languages:Theory and Practice (LFMTP) },
  year =        2006,
  address =     {Seattle, WA, USA},
  month =       aug
}

This material is based upon work supported by the National Science Foundation under Grant No. 0551589. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.
Stephanie Weirich