A solution to the POPLmark challenge using the Matita interactive theorem prover

by Wilmer Ricciotti (ricciott AT cs.unibo.it)

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 language
  • defn.ma, including the definition of the object language in the locally nameless encoding, as well as the basic results needed to prove the main theorems
  • part1a.ma, including the main theorems for the locally nameless encoding.
  • defndb.ma, similar to defn.ma, but in the pure de Bruijn encoding
  • part1adb.ma, similar to part1adb.ma, but in the pure de Bruijn encoding
  • adeq.ma, providing the translation from the locally nameless encoding to the named variables encoding, and a proof of adequacy.