Author: Ralph Matthes
Title: Truly nested datatypes through dependent datatypes - a challenge for Coq
Abstract: 
Following ideas by A. Setzer and P. Aczel, a predicative justification
of the truly nested rank-2 datatype Lam^ representing untyped
lambda-terms that also have a notion of explicit flattening (a weak
form of explicit substitution that blocks beta-redexes) is given by an
implementation within Coq. The true nesting is turned into a
strictly-positive inductive family that is indexed over finite lists
of booleans. Implementing the complete beta-developments for the
heterogeneous rank-2 datatype Lam for pure lambda-terms by help of
Lam^ turned out to be a challenge for pattern-matching definitions and
the program extraction mechanism of Coq.