## 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.