We apply this technique to the POPLmark challenge and experimentally evaluate its efficiency by formalizing System Fsub in the Coq proof assistant in a number of different ways. An analysis of our Coq developments shows that eliminating typing contexts produces a more significant reduction in both the number of lemmas and the count of tactics than the cofinite quantification, one of the most effective ways of simplifying the mechanization involving binders. Our experiment with System Fsub suggests three guidelines to follow when applying the technique of eliminating typing contexts.
The proof scripts along with required libraries can be downloaded as a gzip'd tarball [coq.tar.gz] or a zip file [coq.zip]. Extracting the files creates a subdirectory coq, and you can compile the proof scripts by typing make or make coq. You can generate all the documents using coqdoc by typing make doc. We have tested all the proof scripts on Coq 8.3pl2 (October 2011) and 8.4beta (December 2011). (However the proof scripts do not compile on 8.2pl3.) Our Coq developments for System Fsub use [LibTactics.v] by Arthur Charguéraud (for System Fsub) and the metatheory library by Penn PLClub (for System F^O), both of which are included in our distribution. (We updated the metatheory library for Coq 8.3 and 8.4, but it does not fix all problems and some tactics such as fsetdec still do not work correctly.)
Type safety of System Fsub:
Coq development | Representation | Typing context | Quantification | Definitions (Inductive + Fixpoint) | Lemmas | Tactics | Proof script | Documentation with proofs | Documentation without proofs |
Ours (1) | Locally named | yes | exists-fresh | 25 (12 + 13) | 126 | 2586 | Fnamedcontext.v | HTML | HTML |
Ours (2) | Locally named | yes | cofinite | 23 (10 + 13) | 89 | 1682 | Fnamedcontextcofinite.v | HTML | HTML |
Ours (3) | Locally named | no | exists-fresh | 22 (10 + 12) | 72 | 1176 | Fnamed.v | HTML | HTML |
Ours (4) | Locally named | no | cofinite | 19 (8 + 11) | 50 | 813 | Fnamedcofinite.v | HTML | HTML |
Ours (3') | Locally nameless | no | exists-fresh | 22 (10 + 12) | 72 | 1184 | Fnameless.v | HTML | HTML |
Ours (4') | Locally nameless | no | cofinite | 19 (8 + 11) | 50 | 819 | Fnamelesscofinite.v | HTML | HTML |
Equivalence result between (1) and (3) | Locally named | yes/no | exists-fresh | 42 (17 + 25) | 141 | 2242 | Fequiv.v | HTML | HTML |
Leroy [1] | Locally nameless | yes | for-all | 29 (13 + 16) | 119 | (2128) | [link] | ||
Aydemir et al. [2] | Locally nameless | yes | cofinite | 20 (11 + 9) | 65 | (747) |
Type safety of System F^O:
Coq development | Representation | Non-linear typing context | Quantification | Definitions (Inductive + Fixpoint) | Lemmas | Tactics | Proof script | Documentation | Documentation with proofs |
Ours | Locally nameless | no | cofinite | 21 (11 + 10) | 86 | 1724 | Flinear.v | HTML | HTML |
Mazurak et al. [3] | Locally nameless | yes | cofinite | 25 (14 + 11) | 107 | 2195 |
Programming Language Laboratory Department of Computer Science and Engineering Pohang University of Science and Technology (POSTECH) Republic of Korea