biblio.bib

@String{jfp   = "Journal of Functional Programming"}
@String{lncs  = "Lecture Notes in Computer Science"}
@String{lnai  = "Lecture Notes in Artificial Intelligence"}
@String{SV    = "{Springer-Verlag}"}

@InCollection{Asp00,
  Title        = {Proof General: A Generic Tool for Proof Development},
  Author       = {Aspinall, David},
  Booktitle    = {Tools and Algorithms for the Construction and
               Analysis of Systems, {TACAS} 2000},
  Publisher    = {Springer Berlin Heidelberg},
  Year         = {2000},
  Editor       = {Graf, Susanne and Schwartzbach, Michael},
  Pages        = {38--43},
  Series       = {Lecture Notes in Computer Science},
  Volume       = {1785},
  Doi          = {10.1007/3-540-46419-0_3},
  ISBN         = {978-3-540-67282-1},
}

@Book{Bar81,
  author      = {H.P. Barendregt},
  publisher   = {North-Holland},
  title       = {The Lambda Calculus its Syntax and Semantics},
  year        = {1981}
}

@InProceedings{Bou97,
  title       = {Using reflection to build efficient and certified decision procedure
s},
  author      = {S. Boutin},
  booktitle   = {TACS'97},
  editor      = {Martin Abadi and Takahashi Ito},
  publisher   = SV,
  series      = lncs,
  volume      = 1281,
  year        = {1997}
}

@Article{Bru72,
  author      = {N.J. de Bruijn},
  journal     = {Indag. Math.},
  title       = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}},
  volume      = {34},
  year        = {1972}
}

@inproceedings{CH85,
  title={Constructions: a higher order proof system for mechanizing mathematics},
  author={Coquand, Thierry and Huet, Gérard},
  booktitle={European Conference on Computer Algebra},
  pages={151--184},
  year={1985},
  issn         = {1611-3349},
  doi          = {10.1007/3-540-15983-5_13},
  url          = {http://dx.doi.org/10.1007/3-540-15983-5_13},
  isbn         = 9783540396840,
  publisher    = {Springer Berlin Heidelberg}
}

@techreport{CH88
  TITLE = {{The calculus of constructions}},
  AUTHOR = {Coquand, T. and Huet, G{\'e}rard},
  URL = {https://hal.inria.fr/inria-00076024},
  NUMBER = {RR-0530},
  INSTITUTION = {{INRIA}},
  YEAR = {1986},
  MONTH = May,
  PDF = {https://hal.inria.fr/inria-00076024/file/RR-0530.pdf},
  HAL_ID = {inria-00076024},
  HAL_VERSION = {v1},
}

@techreport{CH87,
  TITLE = {{Concepts mathematiques et informatiques formalises dans le calcul des constructions}},
  AUTHOR = {Coquand, T. and Huet, G{\'e}rard},
  URL = {https://hal.inria.fr/inria-00076039},
  NUMBER = {RR-0515},
  INSTITUTION = {{INRIA}},
  YEAR = {1986},
  MONTH = Apr,
  PDF = {https://hal.inria.fr/inria-00076039/file/RR-0515.pdf},
  HAL_ID = {inria-00076039},
  HAL_VERSION = {v1},
}

@techreport{C90,
  TITLE = {{Metamathematical investigations of a calculus of constructions}},
  AUTHOR = {Coquand, T.},
  URL = {https://hal.inria.fr/inria-00075471},
  NUMBER = {RR-1088},
  INSTITUTION = {{INRIA}},
  YEAR = {1989},
  MONTH = Sep,
  PDF = {https://hal.inria.fr/inria-00075471/file/RR-1088.pdf},
  HAL_ID = {inria-00075471},
  HAL_VERSION = {v1},
}

@PhDThesis{Coq85,
  author      = {Th. Coquand},
  month       = jan,
  school      = {Universit\'e Paris~7},
  title       = {Une Th\'eorie des Constructions},
  year        = {1985}
}

@InProceedings{Coq86,
  author      = {Th. Coquand},
  address     = {Cambridge, MA},
  booktitle   = {Symposium on Logic in Computer Science},
  publisher   = {IEEE Computer Society Press},
  title       = {{An Analysis of Girard's Paradox}},
  year        = {1986}
}

@InProceedings{Coq92,
  author      = {Th. Coquand},
  title       = {{Pattern Matching with Dependent Types}},
  year        = {1992},
  booktitle   = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}
}

@InProceedings{DBLP:conf/types/CornesT95,
  author    = {Cristina Cornes and
               Delphine Terrasse},
  title     = {Automating Inversion of Inductive Predicates in Coq},
  booktitle = {TYPES},
  year      = {1995},
  pages     = {85-104},
  crossref  = {DBLP:conf/types/1995},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{CP90,
  title={Inductively defined types},
  author={Coquand, Thierry and Paulin, Christine},
  booktitle={COLOG-88},
  pages={50--66},
  year={1990},
  issn         = {1611-3349},
  doi          = {10.1007/3-540-52335-9_47},
  url          = {http://dx.doi.org/10.1007/3-540-52335-9_47},
  isbn         = 9783540469636,
  publisher    = {Springer Berlin Heidelberg}
}

@Book{Cur58,
  author      = {Haskell B. Curry and Robert Feys and William Craig},
  title       = {Combinatory Logic},
  volume      = 1,
  publisher   = "North-Holland",
  year        = 1958,
  note        = {{\S{9E}}},
}

@Article{CSlessadhoc,
 author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek},
 title = {How to Make Ad Hoc Proof Automation Less Ad Hoc},
 journal = {SIGPLAN Not.},
 issue_date = {September 2011},
 volume = {46},
 number = {9},
 month = sep,
 year = {2011},
 issn = {0362-1340},
 pages = {163--175},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/2034574.2034798},
 doi = {10.1145/2034574.2034798},
 acmid = {2034798},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes},
}

@InProceedings{CSwcu,
    hal_id = {hal-00816703},
    url = {http://hal.inria.fr/hal-00816703},
    title = {{Canonical Structures for the working Coq user}},
    author = {Mahboubi, Assia and Tassi, Enrico},
    booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}},
    publisher = {Springer},
    pages = {19-34},
    address = {Rennes, France},
    volume = {7998},
    editor = {Sandrine Blazy and Christine Paulin and David Pichardie },
    series = {LNCS },
    doi = {10.1007/978-3-642-39634-2_5},
    year = {2013},
}

@InProceedings{Del00,
  author      = {Delahaye, D.},
  title       = {A {T}actic {L}anguage for the {S}ystem {Coq}},
  booktitle   = {Proceedings of Logic for Programming and Automated Reasoning
               (LPAR), Reunion Island},
  publisher   = SV,
  series      =  LNCS,
  volume      = {1955},
  pages       = {85--95},
  month       = {November},
  year        = {2000},
  url         = {http://www.lirmm.fr/%7Edelahaye/papers/ltac%20(LPAR%2700).pdf}
}

@Article{Dyc92,
  author      = {Roy Dyckhoff},
  journal     = {The Journal of Symbolic Logic},
  month       = sep,
  number      = {3},
  title       = {Contraction-free sequent calculi for intuitionistic logic},
  volume      = {57},
  year        = {1992}
}

@Book{Fourier,
  author      = {Jean-Baptiste-Joseph Fourier},
  publisher   = {Gauthier-Villars},
  title       = {Fourier's method to solve linear
                 inequations/equations systems.},
  year        = {1890}
}

@article{Gilbert:POPL2019,
 author = {Gilbert, Ga\"{e}tan and Cockx, Jesper and Sozeau, Matthieu and Tabareau, Nicolas},
 title = {{Definitional Proof Irrelevance Without K}},
 journal = {Proc. ACM Program. Lang.},
 issue_date = {January 2019},
 volume = {3},
 number = {POPL},
 year = {2019},
 issn = {2475-1421},
 pages = {3:1--3:28},
 articleno = {3},
 numpages = {28},
 url = {http://doi.acm.org/10.1145/3290316},
 acmid = {3290316},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {proof assistants, proof irrelevance, type theory},
}

@InProceedings{Gim94,
  author      = {E. Gim\'enez},
  booktitle   = {Types'94 : Types for Proofs and Programs},
  note        = {Extended version in LIP research report 95-07, ENS Lyon},
  publisher   = SV,
  series      = LNCS,
  title       = {Codifying guarded definitions with recursive schemes},
  volume      = {996},
  year        = {1994}
}

@TechReport{Gim98,
  author      = {E. Gim\'enez},
  title       = {A Tutorial on Recursive Types in Coq},
  institution = {INRIA},
  year        = 1998,
  month       = mar
}

@Unpublished{GimCas05,
  author      = {E. Gim\'enez and P. Cast\'eran},
  title       = {A Tutorial on [Co-]Inductive Types in Coq},
  institution = {INRIA},
  year        = 2005,
  month       = jan,
  note        = {available at \url{http://coq.inria.fr/doc}}
}

@InProceedings{Gimenez95b,
  author      = {E. Gim\'enez},
  booktitle   = {Workshop on Types for Proofs and Programs},
  series      = LNCS,
  number      = {1158},
  pages       = {135-152},
  title       = {An application of co-Inductive types in Coq:
                 verification of the Alternating Bit Protocol},
  editorS     = {S. Berardi and M. Coppo},
  publisher   = SV,
  year        = {1995}
}

@Book{Gir89,
  author      = {J.-Y. Girard and Y. Lafont and P. Taylor},
  publisher   = {Cambridge University Press},
  series      = {Cambridge Tracts in Theoretical Computer Science 7},
  title       = {Proofs and Types},
  year        = {1989}
}

@InCollection{How80,
  author      = {W.A. Howard},
  booktitle   = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
  editor      = {J.P. Seldin and J.R. Hindley},
  note        = {Unpublished 1969 Manuscript},
  publisher   = {Academic Press},
  title       = {The Formulae-as-Types Notion of Constructions},
  year        = {1980}
}

@inproceedings{H88,
  title={Induction principles formalized in the Calculus of Constructions},
  author={Huet, G{\'e}rard},
  booktitle={Programming of Future Generation Computers. Elsevier Science},
  year={1988},
  issn         = {1611-3349},
  doi          = {10.1007/3-540-17660-8_62},
  url          = {http://dx.doi.org/10.1007/3-540-17660-8_62},
  isbn         = 9783540477464,
  publisher    = {Springer Berlin Heidelberg}
}

@InProceedings{H89,
  author      = {G. Huet},
  booktitle   = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
  editor      = {R. Narasimhan},
  publisher   = {World Scientific Publishing},
  title       = {{The Constructive Engine}},
  year        = {1989}
}

@Article{LeeWerner11,
  author    = {Gyesik Lee and
               Benjamin Werner},
  title     = {Proof-irrelevant model of {CC} with predicative induction
               and judgmental equality},
  journal   = {Logical Methods in Computer Science},
  volume    = {7},
  number    = {4},
  year      = {2011},
  ee        = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TechReport{Leroy90,
  author      = {X. Leroy},
  title       = {The {ZINC} experiment: an economical implementation of the {ML} language},
  institution = {INRIA},
  number      = {117},
  year        = {1990}
}

@InProceedings{Let02,
  author      = {P. Letouzey},
  title       = {A New Extraction for Coq},
  booktitle   = {TYPES},
  year        = 2002,
  crossref    = {DBLP:conf/types/2002},
  url         = {http://www.irif.fr/~letouzey/download/extraction2002.pdf}
}

@InProceedings{Luttik97specificationof,
  author = {Sebastiaan P. Luttik and Eelco Visser},
  booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing},
  publisher = SV,
  title = {Specification of Rewriting Strategies},
  year = {1997}
}

@inproceedings{Visser98,
  author    = {Eelco Visser and
               Zine{-}El{-}Abidine Benaissa and
               Andrew P. Tolmach},
  title     = {Building Program Optimizers with Rewriting Strategies},
  booktitle = {ICFP},
  pages     = {13--26},
  year      = {1998},
}

@inproceedings{Visser01,
  author    = {Eelco Visser},
  title     = {Stratego: {A} Language for Program Transformation Based on Rewriting
               Strategies},
  booktitle = {RTA},
  pages     = {357--362},
  year      = {2001},
  series    = {LNCS},
  volume    = {2051},
}

@InProceedings{DBLP:conf/types/McBride00,
  author    = {Conor McBride},
  title     = {Elimination with a Motive},
  booktitle = {TYPES},
  year      = {2000},
  pages     = {197-216},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm},
  crossref  = {DBLP:conf/types/2000},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{Moh93,
  author      = {C. Paulin-Mohring},
  booktitle   = {Proceedings of the conference Typed Lambda Calculi and Applications},
  editor      = {M. Bezem and J.-F. Groote},
  note        = {Also LIP research report 92-49, ENS Lyon},
  number      = {664},
  publisher   = SV,
  series      = {LNCS},
  title       = {{Inductive Definitions in the System Coq - Rules and Properties}},
  year        = {1993}
}

@MastersThesis{Mun94,
  author      = {C. Muñoz},
  month       = sep,
  school      = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
  title       = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
  year        = {1994}
}

@Article{Myers,
  author    = {Eugene Myers},
  title     = {An {O(ND)} difference algorithm and its variations},
  journal   = {Algorithmica},
  volume    = {1},
  number    = {2},
  year      = {1986},
  bibsource = {https://link.springer.com/article/10.1007\%2FBF01840446},
  url       = {http://www.xmailserver.org/diff2.pdf}
}

@inproceedings{P86,
  title={Algorithm development in the calculus of constructions},
  author={Mohring, Christine},
  booktitle={LICS},
  pages={84--91},
  year={1986}
}

@inproceedings{P89,
  title={Extracting $\Omega$'s programs from proofs in the calculus of constructions},
  author={Paulin-Mohring, Christine},
  booktitle={Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  pages={89--104},
  year={1989},
  doi          = {10.1145/75277.75285},
  url          = {http://dx.doi.org/10.1145/75277.75285},
  isbn         = 0897912942,
  organization = {ACM Press}
}

@inproceedings{P93,
  title={Inductive definitions in the system coq rules and properties},
  author={Paulin-Mohring, Christine},
  booktitle={International Conference on Typed Lambda Calculi and Applications},
  pages={328--345},
  year={1993},
  doi          = {10.1007/bfb0037116},
  url          = {http://dx.doi.org/10.1007/bfb0037116},
  isbn         = 3540565175,
  organization = {Springer-Verlag}
}

@inproceedings{PP90,
  title={Inductively defined types in the Calculus of Constructions},
  author={Pfenning, Frank and Paulin-Mohring, Christine},
  booktitle={International Conference on Mathematical Foundations of Programming Semantics},
  pages={209--228},
  year={1989},
  doi          = {10.1007/bfb0040259},
  url          = {http://dx.doi.org/10.1007/bfb0040259},
  isbn         = 0387973753,
  organization = {Springer-Verlag}
}

@InProceedings{Parent95b,
  author      = {C. Parent},
  booktitle   = {{Mathematics of Program Construction'95}},
  publisher   = SV,
  series      = {LNCS},
  title       = {{Synthesizing proofs from programs in
the Calculus of Inductive Constructions}},
  volume      = {947},
  year        = {1995}
}

@InProceedings{Pit16,
  Title        = {Company-Coq: Taking Proof General one step closer to a real IDE},
  Author       = {Pit-Claudel, Clément and Courtieu, Pierre},
  Booktitle    = {CoqPL'16: The Second International Workshop on Coq for PL},
  Year         = {2016},
  Month        = jan,
  Doi          = {10.5281/zenodo.44331},
}

@Book{RC95,
  author      = {di~Cosmo, R.},
  title       = {Isomorphisms of Types: from $\lambda$-calculus to information
                 retrieval and language design},
  series      = {Progress in Theoretical Computer Science},
  publisher   = {Birkhauser},
  year        = {1995},
  note        = {ISBN-0-8176-3763-X}
}

@Article{Rushby98,
  title       = {Subtypes for Specifications: Predicate Subtyping in
                {PVS}},
  author      = {John Rushby and Sam Owre and N. Shankar},
  journal     = {IEEE Transactions on Software Engineering},
  pages       = {709--720},
  volume      = 24,
  number      = 9,
  month       = sep,
  year        = 1998
}

@InProceedings{sozeau06,
  author = {Matthieu Sozeau},
  title = {Subset Coercions in {C}oq},
  year = {2007},
  booktitle = {TYPES'06},
  pages = {237-252},
  volume = {4502},
  publisher = "Springer",
  series =    {LNCS}
}

@InProceedings{sozeau08,
        Author = {Matthieu Sozeau and Nicolas Oury},
        booktitle = {TPHOLs'08},
        Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf},
        Title = {{F}irst-{C}lass {T}ype {C}lasses},
        Year = {2008},
}

@InProceedings{sugar,
    author = {Alessandro Giovini and Teo Mora and Gianfranco Niesi and Lorenzo Robbiano and Carlo Traverso},
    title = {"One sugar cube, please" or Selection strategies in the Buchberger algorithm},
    booktitle = { Proceedings of the ISSAC'91, ACM Press},
    year = {1991},
    pages = {5--4},
    publisher = {}
}

@Article{TheOmegaPaper,
    author = "W. Pugh",
    title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis",
    journal = "Communication of the ACM",
    pages = "102--114",
    year = "1992",
}

@PhDThesis{Wer94,
  author      = {B. Werner},
  school      = {Universit\'e Paris 7},
  title       = {Une th\'eorie des constructions inductives},
  type        = {Th\`ese de Doctorat},
  year        = {1994}
}

@InProceedings{CompiledStrongReduction,
  author    = {Benjamin Gr{\'{e}}goire and
               Xavier Leroy},
  editor    = {Mitchell Wand and
               Simon L. Peyton Jones},
  title     = {A compiled implementation of strong reduction},
  booktitle = {Proceedings of the Seventh {ACM} {SIGPLAN} International Conference
               on Functional Programming {(ICFP} '02), Pittsburgh, Pennsylvania,
               USA, October 4-6, 2002.},
  pages     = {235--246},
  publisher = {{ACM}},
  year      = {2002},
  url       = {http://doi.acm.org/10.1145/581478.581501},
  doi       = {10.1145/581478.581501},
  timestamp = {Tue, 11 Jun 2013 13:49:16 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/icfp/GregoireL02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@InProceedings{FullReduction,
  author    = {Mathieu Boespflug and
               Maxime D{\'{e}}n{\`{e}}s and
               Benjamin Gr{\'{e}}goire},
  editor    = {Jean{-}Pierre Jouannaud and
               Zhong Shao},
  title     = {Full Reduction at Full Throttle},
  booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
               2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7086},
  pages     = {362--377},
  publisher = {Springer},
  year      = {2011},
  url       = {http://dx.doi.org/10.1007/978-3-642-25379-9_26},
  doi       = {10.1007/978-3-642-25379-9_26},
  timestamp = {Thu, 17 Nov 2011 13:33:48 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{MilnerPrincipalTypeSchemes,
 author = {Damas, Luis and Milner, Robin},
 title = {Principal Type-schemes for Functional Programs},
 booktitle = {Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '82},
 year = {1982},
 isbn = {0-89791-065-6},
 location = {Albuquerque, New Mexico},
 pages = {207--212},
 numpages = {6},
 url = {http://doi.acm.org/10.1145/582153.582176},
 doi = {10.1145/582153.582176},
 acmid = {582176},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@techreport{abel19:failur_normal_impred_type_theor,
  author       = {Andreas Abel AND Thierry Coquand},
  title        = {{Failure of Normalization in Impredicative Type
                  Theory with Proof-Irrelevant Propositional
                  Equality}},
  year         = 2019,
  institution = {Chalmers and Gothenburg University},
}

@inproceedings{ConchonFilliatre07wml,
  author = {Sylvain Conchon and Jean-Christophe Filliâtre},
  title = {A Persistent Union-Find Data Structure},
  booktitle = {ACM SIGPLAN Workshop on ML},
  publisher = {ACM Press},
  pages = {37--45},
  year = 2007,
  address = {Freiburg, Germany},
  month = {October},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-pdf = {https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf},
  url = {https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf},
  abstract = { The problem of disjoint sets, also known as union-find,
  consists in maintaining a partition of a finite set within a data
  structure. This structure provides two operations: a function find
  returning the class of an element and a function union merging two
  classes. An optimal and imperative solution is known since 1975.
  However, the imperative nature of this data structure may be a
  drawback when it is used in a backtracking algorithm. This paper
  details the implementation of a persistent union-find data structure
  as efficient as its imperative counterpart.  To achieve this result,
  our solution makes heavy use of imperative features and thus it is a
  significant example of a data structure whose side effects are
  safely hidden behind a persistent interface.  To strengthen this
  last claim, we also detail a formalization using the Coq proof
  assistant which shows both the correctness of our solution and its
  observational persistence. },
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ML}
}