Publication details

Saarland University Computer Science

Binder Aware Recursion over Well-Scoped de Bruijn Syntax

Jonas Kaiser, Steven Schäfer, Kathrin Stark

Certified Programs and Proofs - 7th International Conference, CPP 2018, Los Angeles, USA, January 8-9, 2018, January 2018

The de Bruijn representation of syntax with binding is commonly used, but flawed when it comes to recursion. As the structural recursion principle associated to an inductive type of expressions is unaware of the binding discipline, each recursive definition requires a separate proof of compatibility with variable instantiation. We solve this problem by extending Allais' notion of syntax traversals to obtain a framework for instantiation-compatible recursion. The framework is general enough to handle multivariate, potentially mutually recursive syntactic systems. With our framework we define variable renaming and instantiation, syntax directed typing and certain unary logical relations for System F. These definitons lead to concise proofs of type preservation, as well as weak and strong normalisation. Our framework is designed to serve as the theoretical foundation of future versions of the Autosubst Coq library. All developments and case studies are formalised in the Coq proof assistant.

Link to Coq formalisation

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy