\[\begin{split}\newcommand{\alors}{\textsf{then}}
\newcommand{\alter}{\textsf{alter}}
\newcommand{\as}{\kw{as}}
\newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)}
\newcommand{\bool}{\textsf{bool}}
\newcommand{\case}{\kw{case}}
\newcommand{\conc}{\textsf{conc}}
\newcommand{\cons}{\textsf{cons}}
\newcommand{\consf}{\textsf{consf}}
\newcommand{\conshl}{\textsf{cons\_hl}}
\newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)}
\newcommand{\emptyf}{\textsf{emptyf}}
\newcommand{\End}{\kw{End}}
\newcommand{\kwend}{\kw{end}}
\newcommand{\EqSt}{\textsf{EqSt}}
\newcommand{\even}{\textsf{even}}
\newcommand{\evenO}{\textsf{even}_\textsf{O}}
\newcommand{\evenS}{\textsf{even}_\textsf{S}}
\newcommand{\false}{\textsf{false}}
\newcommand{\filter}{\textsf{filter}}
\newcommand{\Fix}{\kw{Fix}}
\newcommand{\fix}{\kw{fix}}
\newcommand{\for}{\textsf{for}}
\newcommand{\forest}{\textsf{forest}}
\newcommand{\from}{\textsf{from}}
\newcommand{\Functor}{\kw{Functor}}
\newcommand{\haslength}{\textsf{has\_length}}
\newcommand{\hd}{\textsf{hd}}
\newcommand{\ident}{\textsf{ident}}
\newcommand{\In}{\kw{in}}
\newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)}
\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)}
\newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)}
\newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}}
\newcommand{\injective}{\kw{injective}}
\newcommand{\kw}[1]{\textsf{#1}}
\newcommand{\lb}{\lambda}
\newcommand{\length}{\textsf{length}}
\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
\newcommand{\List}{\textsf{list}}
\newcommand{\lra}{\longrightarrow}
\newcommand{\Match}{\kw{match}}
\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})}
\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})}
\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})}
\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})}
\newcommand{\mto}{.\;}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\nat}{\textsf{nat}}
\newcommand{\Nil}{\textsf{nil}}
\newcommand{\nilhl}{\textsf{nil\_hl}}
\newcommand{\nO}{\textsf{O}}
\newcommand{\node}{\textsf{node}}
\newcommand{\nS}{\textsf{S}}
\newcommand{\odd}{\textsf{odd}}
\newcommand{\oddS}{\textsf{odd}_\textsf{S}}
\newcommand{\ovl}[1]{\overline{#1}}
\newcommand{\Pair}{\textsf{pair}}
\newcommand{\plus}{\mathsf{plus}}
\newcommand{\Prod}{\textsf{prod}}
\newcommand{\SProp}{\textsf{SProp}}
\newcommand{\Prop}{\textsf{Prop}}
\newcommand{\return}{\kw{return}}
\newcommand{\Set}{\textsf{Set}}
\newcommand{\si}{\textsf{if}}
\newcommand{\sinon}{\textsf{else}}
\newcommand{\Sort}{\mathcal{S}}
\newcommand{\Str}{\textsf{Stream}}
\newcommand{\Struct}{\kw{Struct}}
\newcommand{\subst}[3]{#1\{#2/#3\}}
\newcommand{\tl}{\textsf{tl}}
\newcommand{\tree}{\textsf{tree}}
\newcommand{\trii}{\triangleright_\iota}
\newcommand{\true}{\textsf{true}}
\newcommand{\Type}{\textsf{Type}}
\newcommand{\unfold}{\textsf{unfold}}
\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}}
\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}}
\newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]}
\newcommand{\WFE}[1]{\WF{E}{#1}}
\newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)}
\newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}
\newcommand{\with}{\kw{with}}
\newcommand{\WS}[3]{#1[] \vdash #2 <: #3}
\newcommand{\WSE}[2]{\WS{E}{#1}{#2}}
\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4}
\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
\newcommand{\zeroone}[1]{[{#1}]}
\newcommand{\zeros}{\textsf{zeros}}
\end{split}\]
Bibliography¶
| [Asp00] | David Aspinall. Proof general: a generic tool for proof development. In Susanne Graf and Michael Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000, volume 1785 of Lecture Notes in Computer Science, pages 38–43. Springer Berlin Heidelberg, 2000. doi:10.1007/3-540-46419-0_3. |
| [Bar81] | H.P. Barendregt. The Lambda Calculus its Syntax and Semantics. North-Holland, 1981. |
| [BDenesGregoire11] | Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. Full reduction at full throttle. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, 362–377. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-25379-9_26, doi:10.1007/978-3-642-25379-9_26. |
| [Bou97] | S. Boutin. Using reflection to build efficient and certified decision procedure s. In Martin Abadi and Takahashi Ito, editors, TACS'97, volume 1281 of Lecture Notes in Computer Science. Springer-Verlag, 1997. |
| [Coq89] | T. Coquand. Metamathematical investigations of a calculus of constructions. Technical Report RR-1088, INRIA, September 1989. URL: https://hal.inria.fr/inria-00075471. |
| [CH86a] | T. Coquand and Gérard Huet. Concepts mathematiques et informatiques formalises dans le calcul des constructions. Technical Report RR-0515, INRIA, April 1986. URL: https://hal.inria.fr/inria-00076039. |
| [CH86b] | T. Coquand and Gérard Huet. The calculus of constructions. Technical Report RR-0530, INRIA, May 1986. URL: https://hal.inria.fr/inria-00076024. |
| [Coq85] | Th. Coquand. Une Théorie des Constructions. PhD thesis, Université Paris 7, January 1985. |
| [Coq86] | Th. Coquand. An Analysis of Girard's Paradox. In Symposium on Logic in Computer Science. Cambridge, MA, 1986. IEEE Computer Society Press. |
| [Coq92] | Th. Coquand. Pattern Matching with Dependent Types. In Proceedings of the 1992 Workshop on Types for Proofs and Programs. 1992. |
| [CH85] | Thierry Coquand and Gérard Huet. Constructions: a higher order proof system for mechanizing mathematics. In European Conference on Computer Algebra, 151–184. Springer Berlin Heidelberg, 1985. URL: http://dx.doi.org/10.1007/3-540-15983-5_13, doi:10.1007/3-540-15983-5_13. |
| [CP90] | Thierry Coquand and Christine Paulin. Inductively defined types. In COLOG-88, 50–66. Springer Berlin Heidelberg, 1990. URL: http://dx.doi.org/10.1007/3-540-52335-9_47, doi:10.1007/3-540-52335-9_47. |
| [CT95] | Cristina Cornes and Delphine Terrasse. Automating inversion of inductive predicates in coq. In TYPES, 85–104. 1995. |
| [CFC58] | Haskell B. Curry, Robert Feys, and William Craig. Combinatory Logic. Volume 1. North-Holland, 1958. §9E. |
| [dB72] | N.J. de Bruijn. Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem. Indag. Math., 1972. |
| [Del00] | D. Delahaye. A Tactic Language for the System Coq. In Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island, volume 1955 of Lecture Notes in Computer Science, 85–95. Springer-Verlag, November 2000. URL: http://www.lirmm.fr/%7Edelahaye/papers/ltac%20(LPAR%2700).pdf. |
| [dC95] | R. di Cosmo. Isomorphisms of Types: from λ-calculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkhauser, 1995. ISBN-0-8176-3763-X. |
| [Dyc92] | Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. The Journal of Symbolic Logic, September 1992. |
| [GCST19] | Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional Proof Irrelevance Without K. Proc. ACM Program. Lang., 3(POPL):3:1–3:28, 2019. URL: http://doi.acm.org/10.1145/3290316. |
| [Gimenez94] | E. Giménez. Codifying guarded definitions with recursive schemes. In Types'94 : Types for Proofs and Programs, volume 996 of Lecture Notes in Computer Science. Springer-Verlag, 1994. Extended version in LIP research report 95-07, ENS Lyon. |
| [Gimenez95] | E. Giménez. An application of co-inductive types in coq: verification of the alternating bit protocol. In Workshop on Types for Proofs and Programs, number 1158 in Lecture Notes in Computer Science, 135–152. Springer-Verlag, 1995. |
| [Gimenez98] | E. Giménez. A tutorial on recursive types in coq. Technical Report, INRIA, March 1998. |
| [GimenezCasteran05] | E. Giménez and P. Castéran. A tutorial on [co-]inductive types in coq. available at http://coq.inria.fr/doc, January 2005. |
| [GMN+91] | Alessandro Giovini, Teo Mora, Gianfranco Niesi, Lorenzo Robbiano, and Carlo Traverso. "one sugar cube, please" or selection strategies in the buchberger algorithm. In Proceedings of the ISSAC'91, ACM Press, 5–4. 1991. |
| [GLT89] | J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1989. |
| [GZND11] | Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. How to make ad hoc proof automation less ad hoc. SIGPLAN Not., 46(9):163–175, September 2011. URL: http://doi.acm.org/10.1145/2034574.2034798, doi:10.1145/2034574.2034798. |
| [GregoireL02] | Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Mitchell Wand and Simon L. Peyton Jones, editors, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002., 235–246. ACM, 2002. URL: http://doi.acm.org/10.1145/581478.581501, doi:10.1145/581478.581501. |
| [How80] | W.A. Howard. The formulae-as-types notion of constructions. In J.P. Seldin and J.R. Hindley, editors, to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980. |
| [Hue89] | G. Huet. The Constructive Engine. In R. Narasimhan, editor, A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney. World Scientific Publishing, 1989. |
| [Hue88] | Gérard Huet. Induction principles formalized in the calculus of constructions. In Programming of Future Generation Computers. Elsevier Science. Springer Berlin Heidelberg, 1988. URL: http://dx.doi.org/10.1007/3-540-17660-8_62, doi:10.1007/3-540-17660-8_62. |
| [LW11] | Gyesik Lee and Benjamin Werner. Proof-irrelevant model of CC with predicative induction and judgmental equality. Logical Methods in Computer Science, 2011. |
| [Ler90] | X. Leroy. The ZINC experiment: an economical implementation of the ML language. Technical Report 117, INRIA, 1990. |
| [Let02] | P. Letouzey. A new extraction for coq. In TYPES. 2002. URL: http://www.irif.fr/~letouzey/download/extraction2002.pdf. |
| [LV97] | Sebastiaan P. Luttik and Eelco Visser. Specification of rewriting strategies. In 2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing. Springer-Verlag, 1997. |
| [MT13] | Assia Mahboubi and Enrico Tassi. Canonical Structures for the working Coq user. In Sandrine Blazy, Christine Paulin, and David Pichardie, editors, ITP 2013, 4th Conference on Interactive Theorem Proving, volume 7998 of LNCS, 19–34. Rennes, France, 2013. Springer. URL: http://hal.inria.fr/hal-00816703, doi:10.1007/978-3-642-39634-2_5. |
| [McB00] | Conor McBride. Elimination with a motive. In TYPES, 197–216. 2000. |
| [Moh86] | Christine Mohring. Algorithm development in the calculus of constructions. In LICS, 84–91. 1986. |
| [Mun94] | C. Muñoz. Démonstration automatique dans la logique propositionnelle intuitionniste. Master's thesis, DEA d'Informatique Fondamentale, Université Paris 7, September 1994. |
| [Mye86] | Eugene Myers. An O(ND) difference algorithm and its variations. Algorithmica, 1986. URL: http://www.xmailserver.org/diff2.pdf. |
| [Par95] | C. Parent. Synthesizing proofs from programs in the Calculus of Inductive Constructions. In Mathematics of Program Construction'95, volume 947 of LNCS. Springer-Verlag, 1995. |
| [PM93a] | C. Paulin-Mohring. Inductive Definitions in the System Coq - Rules and Properties. In M. Bezem and J.-F. Groote, editors, Proceedings of the conference Typed Lambda Calculi and Applications, number 664 in LNCS. Springer-Verlag, 1993. Also LIP research report 92-49, ENS Lyon. |
| [PM89] | Christine Paulin-Mohring. Extracting ω's programs from proofs in the calculus of constructions. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 89–104. ACM Press, 1989. URL: http://dx.doi.org/10.1145/75277.75285, doi:10.1145/75277.75285. |
| [PM93b] | Christine Paulin-Mohring. Inductive definitions in the system coq rules and properties. In International Conference on Typed Lambda Calculi and Applications, 328–345. Springer-Verlag, 1993. URL: http://dx.doi.org/10.1007/bfb0037116, doi:10.1007/bfb0037116. |
| [PPM89] | Frank Pfenning and Christine Paulin-Mohring. Inductively defined types in the calculus of constructions. In International Conference on Mathematical Foundations of Programming Semantics, 209–228. Springer-Verlag, 1989. URL: http://dx.doi.org/10.1007/bfb0040259, doi:10.1007/bfb0040259. |
| [PCC16] | Clément Pit-Claudel and Pierre Courtieu. Company-coq: taking proof general one step closer to a real ide. In CoqPL'16: The Second International Workshop on Coq for PL. January 2016. doi:10.5281/zenodo.44331. |
| [Pug92] | W. Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. Communication of the ACM, pages 102–114, 1992. |
| [ROS98] | John Rushby, Sam Owre, and N. Shankar. Subtypes for specifications: predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24(9):709–720, September 1998. |
| [Soz07] | Matthieu Sozeau. Subset coercions in Coq. In TYPES'06, volume 4502 of LNCS, 237–252. Springer, 2007. |
| [SO08] | Matthieu Sozeau and Nicolas Oury. First-Class Type Classes. In TPHOLs'08. 2008. |
| [Vis01] | Eelco Visser. Stratego: A language for program transformation based on rewriting strategies. In RTA, volume 2051 of LNCS, 357–362. 2001. |
| [VBT98] | Eelco Visser, Zine-El-Abidine Benaissa, and Andrew P. Tolmach. Building program optimizers with rewriting strategies. In ICFP, 13–26. 1998. |
| [Wer94] | B. Werner. Une théorie des constructions inductives. PhD thesis, Université Paris 7, 1994. |