\[\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{\Prod}{\textsf{prod}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\cal S} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \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]{{\cal W\!F}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} \newcommand{\WFTWOLINES}[2]{{\cal 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.

[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.

[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 \sf 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.

[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.

[Fou90]

Jean-Baptiste-Joseph Fourier. Fourier's method to solve linear inequations/equations systems. Gauthier-Villars, 1890.

[Gim94]

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.

[Gim95]

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.

[Gim98]

E. Giménez. A tutorial on recursive types in coq. Technical Report, INRIA, March 1998.

[GC05]

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.

[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.

[Mun94]

C. Muñoz. Démonstration automatique dans la logique propositionnelle intuitionniste. Master's thesis, DEA d'Informatique Fondamentale, Université Paris 7, September 1994.

[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.

[PM93]

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.

[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.

[Wer94]

B. Werner. Une théorie des constructions inductives. PhD thesis, Université Paris 7, 1994.