KnowledgeBase » SEMINAR » ID = 713

The Beauty of Nuprl's Uniform Term Representation and How to Reason about those Terms in Coq

by Abhishek Anand
2013

Abstract

Variable bindings are common in the syntax of many formal languages (e.g. predicate logic, integral calculus, functional programming languages). Modulo some syntactic differences, these languages have identical notions of capture avoiding substitutions. The same is true for alpha equality. Implementing these correctly is a non-trivial task. Proving that the implementation is correct adds a whole new level of complexity.

I will show how Nuprl's way of representing binding structures enables uniform reasoning about them. Even though some people have criticized this representation for being too general, it has a tremendous advantage that the implementation and proofs about substitution and alpha equality do not depend on the actual operators in the language. Hence, these machine checked proofs work unchanged when adding new constructs to the language, or when defining a totally different language.

On the other hand, unlike some other approaches, these definitions are not too general and the key properties about substitution and alpha equality can be proven in CIC(Coq) and need not be added as axioms.

Date: October 9, 2013
Time: 4:00 - 5:00 pm
Location: Upson 5130