POPLmark 1a with Named Bound Variables
Aaron Stump · 2005
A solution to the POPLmark challenge part 1a in Coq version 8.0 is described, where names are used for bound variables. The technical complexities associated with using names for bound variables are tamed using two main technical ideas: de Bruijn levels for free variables, and the Barendregt variable convention. The resulting solution stands at around 1250 lines of Coq (as written by a novice Coq user).