This is a solution to part 1a of the POPLmark challenge which I developed as part of my master thesis under the supervision of prof. Andrea Asperti.
The solution was written using the Matita interactive theorem prover under developement at the Department of Computer Science of the University of Bologna. In the solution, we include the proofs for three different encodings of binders: locally nameless, pure de Bruijn, and named variables. The first two are direct proofs, while the last is obtained by translation of terms with named variables to locally nameless terms.
The solution (which is also available as part of the Matita library), is here provided in a single .tgz archive, containing the following files.
util.ma, including few lemmata not really
related to the object languagedefn.ma, including the definition of the
object language in the locally nameless encoding, as well as the basic results
needed to prove the main theoremspart1a.ma, including the main theorems
for the locally nameless encoding.
defndb.ma, similar to defn.ma, but in the pure
de Bruijn encodingpart1adb.ma, similar to part1adb.ma, but in the
pure de Bruijn encodingadeq.ma, providing the translation from the locally nameless
encoding to the named variables encoding, and a proof of adequacy.