\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \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{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#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}{\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{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \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{\Type}{\textsf{Type}} \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}]} \end{split}\]

Bibliography

AC19

Andreas Abel and Thierry Coquand. Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality. Technical Report, Chalmers and Gothenburg University, 2019.

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.

CF07

Sylvain Conchon and Jean-Christophe Filliâtre. A persistent union-find data structure. In ACM SIGPLAN Workshop on ML, 37–45. Freiburg, Germany, October 2007. ACM Press. URL: https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf.

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.

DM82

Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '82, 207–212. New York, NY, USA, 1982. ACM. URL: http://doi.acm.org/10.1145/582153.582176, doi:10.1145/582153.582176.

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.

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. Thèse de Doctorat, Université Paris 7, 1994.