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.

- Download the Coq development as tarball:
- Browse the source files online. Note that the "Project Page" link in the top right corner of the CoqDoc documentation brings you back to this page.
- CoqDoc Table of Contents
- Basic definitions, inlcuding the assumed axioms, finite types and finite mappings, as well as generic properties of abstract reduction systems:
- The framework, as developed in the paper, for various syntactic systems, together with the general concept of graded types:
- Graded Types
- Framework for the Types of System F
- Framework for the Terms and Values of CBV System F
- Framework for the Terms of Standard System F
- The case studies of the paper:
- Preservation of Typing for CBV System F
- Weak Normalisation for CBV System F
- Strong Normalisation for System F with one Constant
- Additional material that is related but not discussed in the paper: