Mechanizing Metatheory without Typing Contexts

Introduction

When mechanizing the metatheory of a programming language, one usually needs many lemmas proving structural properties of typing judgments, such as permutation and weakening. Such structural lemmas are sometimes unnecessary if we eliminate typing contexts by expanding typing judgments into their original hypothetical proofs. This technique of eliminating typing contexts, which has been around since Church, is based on the view that entailment relations, such as typing judgments, are just syntactic tools for displaying only the hypotheses and conclusion of a hypothetical proof while hiding its internal structure.

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.

Coq developments

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      

References

  1. Xavier Leroy. A locally nameless solution to the POPLmark challenge. Research report 6098, INRIA, January 2007.
  2. Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '08, pages 3--15. ACM, 2008.
  3. Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic. Lightweight linear types in System F^O. In Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI '10, pages 77--88. ACM, 2010.

Email us at .

Programming Language Laboratory
Department of Computer Science and Engineering
Pohang University of Science and Technology (POSTECH)
Republic of Korea