From POPLmark

[edit] General information and files

• Author: Wilmer Ricciotti.
• Part(s) addressed: 1a only.
• Proof assistant / theorem prover used: Matita.
• Encoding technique: Locally nameless.

Files for this submission:

• Directly from the author's page.

[edit] Commentary

• This solution was meant as a test case for the Matita, an interactive theorem prover currently under development at the University of Bologna.
• A first version of the solution follows closely Leroy's swap-based approach.
• The current version of the solution follows closely the specifications, through the use of a hybrid inversion/induction principle.
• A formalization of the proof of adequacy for the locally nameless encoding is also provided.