@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 = {}
}

@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}
}

@phdthesis{Zimmermann19,
  author       = {Th{\'{e}}o Zimmermann},
  title        = {Challenges in the collaborative evolution of a proof language and
                  its ecosystem.},
  school       = {Université de Paris, France},
  year         = {2019},
  url          = {https://tel.archives-ouvertes.fr/tel-02451322},
  timestamp    = {Tue, 21 Jul 2020 00:40:54 +0200},
  biburl       = {https://dblp.org/rec/phd/hal/Zimmermann19.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{TotR21,
  author = {Cockx, Jesper and Tabareau, Nicolas and Winterhalter, Th\'{e}o},
  title = {The Taming of the Rew: A Type Theory with Computational Assumptions},
  year = {2021},
  issue_date = {January 2021},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {5},
  number = {POPL},
  url = {https://doi.org/10.1145/3434341},
  doi = {10.1145/3434341},
  abstract = {Dependently typed programming languages and proof assistants such as Agda and Coq rely on computation to automatically simplify expressions during type checking. To overcome the lack of certain programming primitives or logical principles in those systems, it is common to appeal to axioms to postulate their existence. However, one can only postulate the bare existence of an axiom, not its computational behaviour. Instead, users are forced to postulate equality proofs and appeal to them explicitly to simplify expressions, making axioms dramatically more complicated to work with than built-in primitives. On the other hand, the equality reflection rule from extensional type theory solves these problems by collapsing computation and equality, at the cost of having no practical type checking algorithm. This paper introduces Rewriting Type Theory (RTT), a type theory where it is possible to add computational assumptions in the form of rewrite rules. Rewrite rules go beyond the computational capabilities of intensional type theory, but in contrast to extensional type theory, they are applied automatically so type checking does not require input from the user. To ensure type soundness of RTT—as well as effective type checking—we provide a framework where confluence of user-defined rewrite rules can be checked modularly and automatically, and where adding new rewrite rules is guaranteed to preserve subject reduction. The properties of RTT have been formally verified using the MetaCoq framework and an implementation of rewrite rules is already available in the Agda proof assistant.},
  journal = {Proc. ACM Program. Lang.},
  month = {jan},
  articleno = {60},
  numpages = {29},
  keywords = {termination, dependent types, rewriting theory, confluence, type theory}
}