Nested Abstract Syntax in Coq

International audienceWe illustrate Nested Abstract Syntax as a high-level alternative representation of langages with binding constructs, based on nested datatypes. Our running example is a partial solution in the Coq proof assistant to the POPLmark Challenge. The resulting formalization is very compact and does not require any extra library or special logical apparatus. Along the way, we propose an original, high-level perspective on environments