% Bibliography downloaded from https://researchr.org/downloadbibtex/bibliography/type-system-implementation

@inproceedings{SneltingH86,
  title = {Unification in Many-Sorted Algebras as a Device for Incremental Semantic Analysis},
  author = {Gregor Snelting and Wolfgang Henhapl},
  year = {1986},
  tags = {analysis,  algebra, incremental},
  researchr = {https://researchr.org/publication/SneltingH86},
  cites = {0},
  citedby = {0},
  pages = {229-235},
  booktitle = {POPL},
}

@phdthesis{Har85-0,
  title = {Aspects of the Implementation of Type Theory},
  author = {Robert W. Harper},
  year = {1985},
  researchr = {https://researchr.org/publication/Har85-0},
  cites = {0},
  citedby = {0},
  school = {Cornell University},
}

@inproceedings{PientkaP03,
  title = {Optimizing Higher-Order Pattern Unification},
  author = {Brigitte Pientka and Frank Pfenning},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2741&spage=473},
  tags = {optimization},
  researchr = {https://researchr.org/publication/PientkaP03},
  cites = {0},
  citedby = {0},
  pages = {473-487},
  booktitle = {Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
  editor = {Franz Baader},
  volume = {2741},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-40559-3},
}

@article{WeirichCVE19,
  title = {A role for dependent types in Haskell},
  author = {Stephanie Weirich and Pritam Choudhury and Antoine Voizard and Richard A. Eisenberg},
  year = {2019},
  doi = {10.1145/3341705},
  url = {https://doi.org/10.1145/3341705},
  researchr = {https://researchr.org/publication/WeirichCVE19},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
}

@inproceedings{BauerGHPS16,
  title = {Design and Implementation of the Andromeda Proof Assistant},
  author = {Andrej Bauer and Gaëtan Gilbert and Philipp G. Haselwarter and Matija Pretnar and Christopher A. Stone},
  year = {2016},
  doi = {10.4230/LIPIcs.TYPES.2016.5},
  url = {https://doi.org/10.4230/LIPIcs.TYPES.2016.5},
  researchr = {https://researchr.org/publication/BauerGHPS16},
  cites = {0},
  citedby = {0},
  booktitle = {22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia},
  editor = {Silvia Ghilezan and Herman Geuvers and Jelena Ivetic},
  volume = {97},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-95977-065-1},
}

@article{Xi07:0,
  title = {Dependent ML An approach to practical programming with dependent types},
  author = {Hongwei Xi},
  year = {2007},
  doi = {10.1017/S0956796806006216},
  url = {http://dx.doi.org/10.1017/S0956796806006216},
  tags = {programming, systematic-approach},
  researchr = {https://researchr.org/publication/Xi07%3A0},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {17},
  number = {2},
  pages = {215-286},
}

@inproceedings{GregoireL02,
  title = {A compiled implementation of strong reduction},
  author = {Benjamin Grégoire and Xavier Leroy},
  year = {2002},
  doi = {10.1145/581478.581501},
  url = {http://doi.acm.org/10.1145/581478.581501},
  tags = {compiler},
  researchr = {https://researchr.org/publication/GregoireL02},
  cites = {0},
  citedby = {0},
  pages = {235-246},
  booktitle = {Proceedings of the seventh {ACM SIGPLAN} international conference on Functional Programming {(ICFP 2002)}},
}

@inproceedings{Pfenning89,
  title = {Elf: A Language for Logic Definition and Verified Metaprogramming},
  author = {Frank Pfenning},
  year = {1989},
  tags = {logic},
  researchr = {https://researchr.org/publication/Pfenning89},
  cites = {0},
  citedby = {0},
  pages = {313-322},
  booktitle = {Proceedings, Fourth Annual Symposium on Logic in Computer Science, 5-8 June, 1989, Asilomar Conference Center, Pacific Grove, California, USA},
  publisher = {IEEE Computer Society},
}

@inproceedings{HondetB20,
  title = {The New Rewriting Engine of Dedukti (System Description)},
  author = {Gabriel Hondet and Frédéric Blanqui},
  year = {2020},
  doi = {10.4230/LIPIcs.FSCD.2020.35},
  url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.35},
  researchr = {https://researchr.org/publication/HondetB20},
  cites = {0},
  citedby = {0},
  booktitle = {5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference)},
  editor = {Zena M. Ariola},
  volume = {167},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-155-9},
}

@article{GaherSJKD24,
  title = {RefinedRust: A Type System for High-Assurance Verification of Rust Programs},
  author = {Lennard Gäher and Michael Sammler and Ralf Jung 0002 and Robbert Krebbers and Derek Dreyer},
  year = {2024},
  doi = {10.1145/3656422},
  url = {https://doi.org/10.1145/3656422},
  researchr = {https://researchr.org/publication/GaherSJKD24},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {PLDI},
  pages = {1115-1139},
}

@misc{frber2021small,
  title = {Small, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting},
  author = {Michael Färber},
  year = {2021},
  researchr = {https://researchr.org/publication/frber2021small},
  cites = {0},
  citedby = {0},
}

@article{Tejiscak20,
  title = {A dependently typed calculus with pattern matching and erasure inference},
  author = {Matus Tejiscak},
  year = {2020},
  doi = {10.1145/3408973},
  url = {https://doi.org/10.1145/3408973},
  researchr = {https://researchr.org/publication/Tejiscak20},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {ICFP},
}

@mastersthesis{hondet:hal-02317471,
  title = {Efficient rewriting using decision trees},
  author = {Hondet, Gabriel},
  year = {2019},
  month = {Aug},
  url = {https://hal.inria.fr/hal-02317471},
  researchr = {https://researchr.org/publication/hondet%3Ahal-02317471},
  cites = {0},
  citedby = {0},
  school = {ENAC ; Univesit{\'e} Toulouse III- Paul Sabatier},
}

@inproceedings{Cockx19,
  title = {Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules},
  author = {Jesper Cockx},
  year = {2019},
  doi = {10.4230/LIPIcs.TYPES.2019.2},
  url = {https://doi.org/10.4230/LIPIcs.TYPES.2019.2},
  researchr = {https://researchr.org/publication/Cockx19},
  cites = {0},
  citedby = {0},
  booktitle = {25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway},
  editor = {Marc Bezem and Assia Mahboubi},
  volume = {175},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-158-0},
}

@inproceedings{SelsamM16,
  title = {Congruence Closure in Intensional Type Theory},
  author = {Daniel Selsam and Leonardo de Moura},
  year = {2016},
  doi = {10.1007/978-3-319-40229-1_8},
  url = {http://dx.doi.org/10.1007/978-3-319-40229-1_8},
  researchr = {https://researchr.org/publication/SelsamM16},
  cites = {0},
  citedby = {0},
  pages = {99-115},
  booktitle = {Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  editor = {Nicola Olivetti and Ashish Tiwari},
  volume = {9706},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-40228-4},
}

@inproceedings{SchurmannP03,
  title = {A Coverage Checking Algorithm for LF},
  author = {Carsten Schürmann and Frank Pfenning},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=120},
  tags = {coverage},
  researchr = {https://researchr.org/publication/SchurmannP03},
  cites = {0},
  citedby = {0},
  pages = {120-135},
  booktitle = {Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings},
  editor = {David A. Basin and Burkhart Wolff},
  volume = {2758},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-40664-6},
}

@article{SozeauM19,
  title = {Equations reloaded: high-level dependently-typed functional programming and proving in Coq},
  author = {Matthieu Sozeau and Cyprien Mangin},
  year = {2019},
  doi = {10.1145/3341690},
  url = {https://doi.org/10.1145/3341690},
  researchr = {https://researchr.org/publication/SozeauM19},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
}

@inproceedings{ChristiansenB16,
  title = {Elaborator reflection: extending Idris in Idris},
  author = {David Christiansen and Edwin Brady},
  year = {2016},
  doi = {10.1145/2951913.2951932},
  url = {http://doi.acm.org/10.1145/2951913.2951932},
  researchr = {https://researchr.org/publication/ChristiansenB16},
  cites = {0},
  citedby = {0},
  pages = {284-297},
  booktitle = {Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016},
  editor = {Jacques Garrigue and Gabriele Keller and Eijiro Sumii},
  publisher = {ACM},
  isbn = {978-1-4503-4219-3},
}

@inproceedings{MouraKADR15,
  title = {The Lean Theorem Prover (System Description)},
  author = {Leonardo Mendonça de Moura and Soonho Kong and Jeremy Avigad and Floris van Doorn and Jakob von Raumer},
  year = {2015},
  doi = {10.1007/978-3-319-21401-6_26},
  url = {http://dx.doi.org/10.1007/978-3-319-21401-6_26},
  researchr = {https://researchr.org/publication/MouraKADR15},
  cites = {0},
  citedby = {0},
  pages = {378-388},
  booktitle = {Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
  editor = {Amy P. Felty and Aart Middeldorp},
  volume = {9195},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-21400-9},
}

@inproceedings{Christiansen14-1,
  title = {Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection},
  author = {David Raymond Christiansen},
  year = {2014},
  doi = {10.1145/2746325.2746326},
  url = {http://doi.acm.org/10.1145/2746325.2746326},
  researchr = {https://researchr.org/publication/Christiansen14-1},
  cites = {0},
  citedby = {0},
  pages = {1},
  booktitle = {Proceedings of the 26th 2014 International Symposium on Implementation and Application of Functional Languages, IFL '14, Boston, MA, USA, October 1-3, 2014},
  editor = {Sam Tobin-Hochstadt},
  publisher = {ACM},
  isbn = {978-1-4503-3284-2},
}

@phdthesis{Norell2007towardsapractical,
  title = {Towards a practical programming language based on dependent type theory},
  author = {Ulf Norell},
  year = {2007},
  month = {September},
  researchr = {https://researchr.org/publication/Norell2007towardsapractical},
  cites = {0},
  citedby = {0},
  school = {Department of Computer Science and Engineering, Chalmers University of Technology},
  address = {SE-412 96 G\"{o}teborg, Sweden},
}

@inproceedings{XiP99,
  title = {Dependent Types in Practical Programming},
  author = {Hongwei Xi and Frank Pfenning},
  year = {1999},
  doi = {10.1145/292540.292560},
  url = {http://doi.acm.org/10.1145/292540.292560},
  tags = {programming},
  researchr = {https://researchr.org/publication/XiP99},
  cites = {0},
  citedby = {0},
  pages = {214-227},
  booktitle = {POPL},
}

@inproceedings{DunchevGCT15,
  title = {ELPI: Fast, Embeddable, \lambda Prolog Interpreter},
  author = {Cvetan Dunchev and Ferruccio Guidi and Claudio Sacerdoti Coen and Enrico Tassi},
  year = {2015},
  doi = {10.1007/978-3-662-48899-7_32},
  url = {http://dx.doi.org/10.1007/978-3-662-48899-7_32},
  researchr = {https://researchr.org/publication/DunchevGCT15},
  cites = {0},
  citedby = {0},
  pages = {460-468},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings},
  editor = {Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov},
  volume = {9450},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-662-48898-0},
}

@misc{dagand2012elaborating,
  title = {Elaborating Inductive Definitions},
  author = {Pierre-Evariste Dagand and Conor McBride},
  year = {2012},
  researchr = {https://researchr.org/publication/dagand2012elaborating},
  cites = {0},
  citedby = {0},
}

@inproceedings{0002M20-2,
  title = {Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages},
  author = {Sebastian Ullrich and Leonardo de Moura},
  year = {2020},
  doi = {10.1007/978-3-030-51054-1_10},
  url = {https://doi.org/10.1007/978-3-030-51054-1_10},
  researchr = {https://researchr.org/publication/0002M20-2},
  cites = {0},
  citedby = {0},
  pages = {167-182},
  booktitle = {Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II},
  editor = {Nicolas Peltier and Viorica Sofronie-Stokkermans},
  volume = {12167},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-51054-1},
}

@book{friedman2018little,
  title = {The Little Typer},
  author = {Friedman, Daniel P and Christiansen, David Thrane},
  year = {2018},
  researchr = {https://researchr.org/publication/friedman2018little},
  cites = {0},
  citedby = {0},
  publisher = {MIT Press},
}

@inproceedings{CallaghanL99,
  title = {Implementation Techniques for Inductive Types in Plastic},
  author = {Paul Callaghan and Zhaohui Luo},
  year = {1999},
  url = {http://link.springer.de/link/service/series/0558/bibs/1956/19560094.htm},
  researchr = {https://researchr.org/publication/CallaghanL99},
  cites = {0},
  citedby = {0},
  pages = {94-113},
  booktitle = {Types for Proofs and Programs, International Workshop TYPES 99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers},
  editor = {Thierry Coquand and Peter Dybjer and Bengt Nordström and Jan M. Smith},
  volume = {1956},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-41517-3},
}

@inproceedings{CheneyU04,
  title = {{$\alpha$Prolog}: A Logic Programming Language with Names, Binding and $\alpha$-Equivalence},
  author = {James Cheney and Christian Urban},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3132&spage=269},
  tags = {programming languages, Prolog, logic programming, programming, logic},
  researchr = {https://researchr.org/publication/CheneyU04},
  cites = {0},
  citedby = {0},
  pages = {269-283},
  booktitle = {Logic Programming, 20th International Conference, ICLP 2004, Saint-Malo, France, September 6-10, 2004, Proceedings},
  editor = {Bart Demoen and Vladimir Lifschitz},
  volume = {3132},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-22671-0},
}

@inproceedings{Despeyroux84,
  title = {Executable Specification of Static Semantics},
  author = {Thierry Despeyroux},
  year = {1984},
  tags = {semantics},
  researchr = {https://researchr.org/publication/Despeyroux84},
  cites = {0},
  citedby = {0},
  pages = {215-233},
  booktitle = {Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27-29, 1984, Proceedings},
  editor = {Gilles Kahn and David B. MacQueen and Gordon D. Plotkin},
  volume = {173},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-13346-1},
}

@inproceedings{AbelCP09,
  title = {A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance},
  author = {Andreas Abel and Thierry Coquand and Miguel Pagano},
  year = {2009},
  doi = {10.1007/978-3-642-02273-9_3},
  url = {http://dx.doi.org/10.1007/978-3-642-02273-9_3},
  tags = {type checking, type theory},
  researchr = {https://researchr.org/publication/AbelCP09},
  cites = {0},
  citedby = {0},
  pages = {5-19},
  booktitle = {Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings},
  editor = {Pierre-Louis Curien},
  volume = {5608},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-02272-2},
}

@article{AspertiCTZ07,
  title = {User Interaction with the Matita Proof Assistant},
  author = {Andrea Asperti and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli},
  year = {2007},
  doi = {10.1007/s10817-007-9070-5},
  url = {http://dx.doi.org/10.1007/s10817-007-9070-5},
  tags = {proof assistant},
  researchr = {https://researchr.org/publication/AspertiCTZ07},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {39},
  number = {2},
  pages = {109-139},
}

@phdthesis{ethos-4985,
  title = {Practical implementation of a dependently typed functional programming language},
  author = {Edwin Brady},
  year = {2005},
  url = {http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.417649},
  note = {British Library, EThOS},
  researchr = {https://researchr.org/publication/ethos-4985},
  cites = {0},
  citedby = {0},
  school = {Durham University, UK},
}

@unpublished{mazzoli2016type,
  title = {Type checking through unification},
  author = {Francesco Mazzoli and Andreas Abel},
  year = {2016},
  researchr = {https://researchr.org/publication/mazzoli2016type},
  cites = {0},
  citedby = {0},
}

@inproceedings{PfenningS99,
  title = {System Description: Twelf - A Meta-Logical Framework for Deductive Systems},
  author = {Frank Pfenning and Carsten Schürmann},
  year = {1999},
  url = {http://link.springer.de/link/service/series/0558/bibs/1632/16320202.htm},
  tags = {meta-model, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/PfenningS99},
  cites = {0},
  citedby = {0},
  pages = {202-206},
  booktitle = {Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings},
  editor = {Harald Ganzinger},
  volume = {1632},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-66222-7},
}

@article{bowman2016growing,
  title = {Growing a proof assistant},
  author = {Bowman, William J},
  year = {2016},
  researchr = {https://researchr.org/publication/bowman2016growing},
  cites = {0},
  citedby = {0},
  journal = {Higher-Order Programming with Effects},
  volume = {65},
}

@article{DBLP:journals-corr-MouraAKR15,
  title = {Elaboration in Dependent Type Theory},
  author = {Leonardo Mendon{\c{c}}a de Moura and Jeremy Avigad and Soonho Kong and Cody Roux},
  year = {2015},
  url = {http://arxiv.org/abs/1505.04324},
  researchr = {https://researchr.org/publication/DBLP%3Ajournals-corr-MouraAKR15},
  cites = {0},
  citedby = {0},
  journal = {CoRR},
  volume = {abs/1505.04324},
}

@inproceedings{Farber22,
  title = {Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting},
  author = {Michael Färber},
  year = {2022},
  doi = {10.1145/3497775.3503683},
  url = {https://doi.org/10.1145/3497775.3503683},
  researchr = {https://researchr.org/publication/Farber22},
  cites = {0},
  citedby = {0},
  pages = {225-238},
  booktitle = {CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
  editor = {Andrei Popescu 0001 and Steve Zdancewic},
  publisher = {ACM},
  isbn = {978-1-4503-9182-5},
}

@article{BahlkeS86:0,
  title = {The {PSG} System: From Formal Language Definitions to Interactive Programming Environments},
  author = {Rolf Bahlke and Gregor Snelting},
  year = {1986},
  doi = {10.1145/6465.20890},
  url = {http://doi.acm.org/10.1145/6465.20890},
  tags = {programming languages, meta programming, programming, Meta-Environment},
  researchr = {https://researchr.org/publication/BahlkeS86%3A0},
  cites = {0},
  citedby = {2},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {8},
  number = {4},
  pages = {547-576},
}

@phdthesis{ethos-1465,
  title = {Type inference, Haskell and dependent types},
  author = {Adam Michael Gundry},
  year = {2013},
  url = {http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.605927},
  note = {British Library, EThOS},
  researchr = {https://researchr.org/publication/ethos-1465},
  cites = {0},
  citedby = {0},
  school = {University of Strathclyde, Glasgow, UK},
}

@inproceedings{Setzer0PT14,
  title = {Unnesting of Copatterns},
  author = {Anton Setzer and Andreas Abel and Brigitte Pientka and David Thibodeau},
  year = {2014},
  doi = {10.1007/978-3-319-08918-8_3},
  url = {http://dx.doi.org/10.1007/978-3-319-08918-8_3},
  researchr = {https://researchr.org/publication/Setzer0PT14},
  cites = {0},
  citedby = {0},
  pages = {31-45},
  booktitle = {Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings},
  editor = {Gilles Dowek},
  volume = {8560},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-08917-1},
}

@inproceedings{000110-2,
  title = {MiniAgda: Integrating Sized and Dependent Types},
  author = {Andreas Abel},
  year = {2010},
  url = {http://www.easychair.org/publications/?page=506004245},
  researchr = {https://researchr.org/publication/000110-2},
  cites = {0},
  citedby = {0},
  pages = {18-32},
  booktitle = {Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010},
  editor = {Ekaterina Komendantskaya and Ana Bove and Milad Niqui},
  volume = {5},
  series = {EPiC Series},
  publisher = {EasyChair},
}

@inproceedings{RohwedderP96,
  title = {Mode and Termination Checking for Higher-Order Logic Programs},
  author = {Ekkehard Rohwedder and Frank Pfenning},
  year = {1996},
  tags = {termination, logic programming, logic},
  researchr = {https://researchr.org/publication/RohwedderP96},
  cites = {0},
  citedby = {0},
  pages = {296-310},
  booktitle = {Programming Languages and Systems - ESOP 96, 6th European Symposium on Programming, Linköping, Sweden, April 22-24, 1996, Proceedings},
  editor = {Hanne Riis Nielson},
  volume = {1058},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-61055-3},
}

@inproceedings{ChapmanAM05,
  title = {Epigram reloaded: a standalone typechecker for ETT},
  author = {James Chapman and Thorsten Altenkirch and Conor McBride},
  year = {2005},
  researchr = {https://researchr.org/publication/ChapmanAM05},
  cites = {0},
  citedby = {0},
  pages = {79-94},
  booktitle = {Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24 September 2005},
  editor = {Marko C. J. D. van Eekelen},
  volume = {6},
  series = {Trends in Functional Programming},
  publisher = {Intellect},
  isbn = {978-1-84150-176-5},
}

@phdthesis{ethos-7403,
  title = {The theory of LEGO},
  author = {Robert Pollack},
  year = {1995},
  url = {http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.561652},
  note = {British Library, EThOS},
  researchr = {https://researchr.org/publication/ethos-7403},
  cites = {0},
  citedby = {0},
}

@inproceedings{McBrideM04-0,
  title = {Functional pearl: I am not a number-I am a free variable},
  author = {Conor McBride and James McKinna},
  year = {2004},
  doi = {10.1145/1017472.1017477},
  url = {http://doi.acm.org/10.1145/1017472.1017477},
  researchr = {https://researchr.org/publication/McBrideM04-0},
  cites = {0},
  citedby = {0},
  pages = {1-9},
  booktitle = {Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004, Snowbird, UT, USA, September 22-22, 2004},
  editor = {Henrik Nilsson},
  publisher = {ACM},
}

@article{Kovacs20,
  title = {Elaboration with first-class implicit function types},
  author = {András Kovács},
  year = {2020},
  doi = {10.1145/3408983},
  url = {https://doi.org/10.1145/3408983},
  researchr = {https://researchr.org/publication/Kovacs20},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {ICFP},
}

@article{Coquand96,
  title = {An Algorithm for Type-Checking Dependent Types},
  author = {Thierry Coquand},
  year = {1996},
  tags = {type checking},
  researchr = {https://researchr.org/publication/Coquand96},
  cites = {0},
  citedby = {0},
  journal = {Science of Computer Programming},
  volume = {26},
  number = {1-3},
  pages = {167-177},
}

@phdthesis{hal-8150,
  title = {Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique)},
  author = {Ronan Saillard},
  year = {2015},
  url = {https://tel.archives-ouvertes.fr/tel-01299180},
  researchr = {https://researchr.org/publication/hal-8150},
  cites = {0},
  citedby = {0},
  school = {Mines ParisTech, France},
}

@article{GuidiCT19,
  title = {Implementing type theory in higher order constraint logic programming},
  author = {Ferruccio Guidi and Claudio Sacerdoti Coen and Enrico Tassi},
  year = {2019},
  doi = {10.1017/S0960129518000427},
  url = {https://doi.org/10.1017/S0960129518000427},
  researchr = {https://researchr.org/publication/GuidiCT19},
  cites = {0},
  citedby = {0},
  journal = {Mathematical Structures in Computer Science},
  volume = {29},
  number = {8},
  pages = {1125-1150},
}

@article{GratzerSB19,
  title = {Implementing a modal dependent type theory},
  author = {Daniel Gratzer and Jonathan Sterling and Lars Birkedal},
  year = {2019},
  doi = {10.1145/3341711},
  url = {https://doi.org/10.1145/3341711},
  researchr = {https://researchr.org/publication/GratzerSB19},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
}

@article{VytiniotisJSS11,
  title = {{OutsideIn(X)} Modular type inference with local assumptions},
  author = {Dimitrios Vytiniotis and Simon L. Peyton Jones and Tom Schrijvers and Martin Sulzmann},
  year = {2011},
  tags = {empirical, programming languages, type inference, rule-based, data-flow language, constraints, Haskell, type system, data-flow programming, data-flow, metatheory, systematic-approach, local type inference, domain-specific language},
  researchr = {https://researchr.org/publication/VytiniotisJSS11},
  cites = {0},
  citedby = {0},
  journal = {J. Funct. Program.},
  volume = {21},
  number = {4-5},
  pages = {333-412},
}

@article{norell2007type,
  title = {Type checking in the presence of meta-variables},
  author = {Norell, Ulf and Coquand, Catarina},
  year = {2007},
  researchr = {https://researchr.org/publication/norell2007type},
  cites = {0},
  citedby = {0},
}

@inproceedings{AspertiCTZ06,
  title = {Crafting a Proof Assistant},
  author = {Andrea Asperti and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli},
  year = {2006},
  doi = {10.1007/978-3-540-74464-1_2},
  url = {http://dx.doi.org/10.1007/978-3-540-74464-1_2},
  tags = {proof assistant},
  researchr = {https://researchr.org/publication/AspertiCTZ06},
  cites = {0},
  citedby = {0},
  pages = {18-32},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
  editor = {Thorsten Altenkirch and Conor McBride},
  volume = {4502},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-74463-4},
}

@article{PfenningS98,
  title = {Algorithms for Equality and Unification in the Presence of Notational Definitions},
  author = {Frank Pfenning and Carsten Schürmann},
  year = {1998},
  url = {http://www.elsevier.com/gej-ng/31/29/23/41/23/show/Products/notes/index.htt#006},
  researchr = {https://researchr.org/publication/PfenningS98},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {17},
  pages = {1-13},
}

@unpublished{Brady2021,
  title = {Idris 2: Quantitative Type Theory in Action},
  author = {Edwin Brady},
  year = {2021},
  researchr = {https://researchr.org/publication/Brady2021},
  cites = {0},
  citedby = {0},
}

@article{Asperti2009,
  title = {A compact kernel for the calculus of inductive constructions},
  author = {A. Asperti and  W. Ricciotti and  Coen Sacerdoti and E. Tassi},
  year = {2009},
  doi = {10.1007/s12046-009-0003-3},
  researchr = {https://researchr.org/publication/Asperti2009},
  cites = {0},
  citedby = {0},
}

@inproceedings{AspertiRCT09,
  title = {Hints in Unification},
  author = {Andrea Asperti and Wilmer Ricciotti and Claudio Sacerdoti Coen and Enrico Tassi},
  year = {2009},
  doi = {10.1007/978-3-642-03359-9_8},
  url = {http://dx.doi.org/10.1007/978-3-642-03359-9_8},
  researchr = {https://researchr.org/publication/AspertiRCT09},
  cites = {0},
  citedby = {0},
  pages = {84-98},
  booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
  editor = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
  volume = {5674},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-03358-2},
}

@article{PierceT-TOPLAS-2000,
  title = {Local type inference},
  author = {Benjamin C. Pierce and David N. Turner},
  year = {2000},
  doi = {10.1145/345099.345100},
  url = {http://doi.acm.org/10.1145/345099.345100},
  tags = {type inference, language design, constraints, C++, subtyping, abstraction, local type inference},
  researchr = {https://researchr.org/publication/PierceT-TOPLAS-2000},
  cites = {54},
  citedby = {0},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {22},
  number = {1},
  pages = {1-44},
}

@inproceedings{Moura021,
  title = {The Lean 4 Theorem Prover and Programming Language},
  author = {Leonardo de Moura and Sebastian Ullrich},
  year = {2021},
  doi = {10.1007/978-3-030-79876-5_37},
  url = {https://doi.org/10.1007/978-3-030-79876-5_37},
  researchr = {https://researchr.org/publication/Moura021},
  cites = {0},
  citedby = {0},
  pages = {625-635},
  booktitle = {Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
  editor = {André Platzer and Geoff Sutcliffe},
  volume = {12699},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-79876-5},
}

@inproceedings{SjobergW15,
  title = {Programming up to Congruence},
  author = {Vilhelm Sjöberg and Stephanie Weirich},
  year = {2015},
  doi = {10.1145/2676726.2676974},
  url = {http://doi.acm.org/10.1145/2676726.2676974},
  researchr = {https://researchr.org/publication/SjobergW15},
  cites = {0},
  citedby = {0},
  pages = {369-382},
  booktitle = {Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015},
  editor = {Sriram K. Rajamani and David Walker},
  publisher = {ACM},
  isbn = {978-1-4503-3300-9},
}

@inproceedings{FerreiraP14-3,
  title = {Bidirectional Elaboration of Dependently Typed Programs},
  author = {Francisco Ferreira and Brigitte Pientka},
  year = {2014},
  doi = {10.1145/2643135.2643153},
  url = {http://doi.acm.org/10.1145/2643135.2643153},
  researchr = {https://researchr.org/publication/FerreiraP14-3},
  cites = {0},
  citedby = {0},
  pages = {161-174},
  booktitle = {Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014},
  editor = {Olaf Chitil and Andy King and Olivier Danvy},
  publisher = {ACM},
  isbn = {978-1-4503-2947-7},
}

@incollection{Huet89,
  title = {The Constructive Engine},
  author = {Gérard Huet},
  year = {1989},
  doi = {10.1142/9789814368452_0004},
  url = {http://dx.doi.org/10.1142/9789814368452_0004},
  researchr = {https://researchr.org/publication/Huet89},
  cites = {0},
  citedby = {0},
  pages = {38-69},
  booktitle = {A Perspective in Theoretical Computer Science - Commemorative Volume for Gift Siromoney},
  editor = {R. Narasimhan},
  volume = {16},
  series = {World Scientific Series in Computer Science},
  publisher = {World Scientific},
  isbn = {978-981-4507-35-6},
}

@article{DBLP:journals-corr-abs-1908-05647,
  title = {Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming},
  author = {Sebastian Ullrich and Leonardo de Moura},
  year = {2019},
  url = {http://arxiv.org/abs/1908.05647},
  researchr = {https://researchr.org/publication/DBLP%3Ajournals-corr-abs-1908-05647},
  cites = {0},
  citedby = {0},
  journal = {CoRR},
  volume = {abs/1908.05647},
}

@inproceedings{BradyMM03,
  title = {Inductive Families Need Not Store Their Indices},
  author = {Edwin Brady and Conor McBride and James McKinna},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3085&spage=115},
  researchr = {https://researchr.org/publication/BradyMM03},
  cites = {0},
  citedby = {0},
  pages = {115-129},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers},
  editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
  volume = {3085},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-22164-6},
}

@article{coquand2009simple,
  title = {A simple type-theoretic language: Mini-TT},
  author = {Thierry Coquand and Yoshiki Kinoshita and Bengt Nordström and Makoto Takeyama},
  year = {2009},
  researchr = {https://researchr.org/publication/coquand2009simple},
  cites = {0},
  citedby = {0},
  journal = {From Semantics to Computer Science; Essays in Honour of Gilles Kahn},
  pages = {139-164},
}

@article{SacerdotiCoen2011,
  title = {Nonuniform Coercions via Unification Hints},
  author = {Sacerdoti Coen, Claudio and Tassi, Enrico},
  year = {2011},
  month = {Mar},
  doi = {10.4204/eptcs.53.2},
  url = {http://dx.doi.org/10.4204/EPTCS.53.2},
  researchr = {https://researchr.org/publication/SacerdotiCoen2011},
  cites = {0},
  citedby = {0},
  journal = {Electronic Proceedings in Theoretical Computer Science},
  volume = {53},
}

@article{LohMS10,
  title = {A Tutorial Implementation of a Dependently Typed Lambda Calculus},
  author = {Andres Löh and Conor McBride and Wouter Swierstra},
  year = {2010},
  doi = {10.3233/FI-2010-304},
  url = {http://dx.doi.org/10.3233/FI-2010-304},
  researchr = {https://researchr.org/publication/LohMS10},
  cites = {0},
  citedby = {0},
  journal = {Fundamenta Informaticae},
  volume = {102},
  number = {2},
  pages = {177-207},
}

@article{Brady13-Idris,
  title = {Idris, a general-purpose dependently typed programming language: Design and implementation},
  author = {Edwin Brady},
  year = {2013},
  doi = {10.1017/S095679681300018X},
  url = {http://dx.doi.org/10.1017/S095679681300018X},
  researchr = {https://researchr.org/publication/Brady13-Idris},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {23},
  number = {5},
  pages = {552-593},
}

@inproceedings{JuttingMP93,
  title = {Checking Algorithms for Pure Type Systems},
  author = {L. S. van Benthem Jutting and James McKinna and Robert Pollack},
  year = {1993},
  tags = {type system, type checking},
  researchr = {https://researchr.org/publication/JuttingMP93},
  cites = {0},
  citedby = {0},
  pages = {19-61},
  booktitle = {Types for Proofs and Programs, International Workshop TYPES 93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers},
  editor = {Henk Barendregt and Tobias Nipkow},
  volume = {806},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-58085-9},
}

@article{ZilianiS17,
  title = {A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading},
  author = {Beta Ziliani and Matthieu Sozeau},
  year = {2017},
  doi = {10.1017/S0956796817000028},
  url = {http://dx.doi.org/10.1017/S0956796817000028},
  researchr = {https://researchr.org/publication/ZilianiS17},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {27},
}

@inproceedings{SammlerLKMD021,
  title = {RefinedC: automating the foundational verification of C code with refined ownership types},
  author = {Michael Sammler and Rodolphe Lepigre and Robbert Krebbers and Kayvan Memarian and Derek Dreyer and Deepak Garg 0001},
  year = {2021},
  doi = {10.1145/3453483.3454036},
  url = {https://doi.org/10.1145/3453483.3454036},
  researchr = {https://researchr.org/publication/SammlerLKMD021},
  cites = {0},
  citedby = {0},
  pages = {158-174},
  booktitle = {PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 20211},
  editor = {Stephen N. Freund and Eran Yahav},
  publisher = {ACM},
  isbn = {978-1-4503-8391-2},
}

@article{LevinP03,
  title = {TinkerType: a language for playing with formal systems},
  author = {Michael Y. Levin and Benjamin C. Pierce},
  year = {2003},
  doi = {10.1017/S0956796802004550},
  url = {http://dx.doi.org/10.1017/S0956796802004550},
  tags = {control systems, semantics, type inference, rule-based, application framework, formal semantics, type system, rules, C++, subtyping, type checking, consistency, operational semantics, logic},
  researchr = {https://researchr.org/publication/LevinP03},
  cites = {31},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {13},
  number = {2},
  pages = {295-316},
}

@article{EbnerURAM17,
  title = {A metaprogramming framework for formal verification},
  author = {Gabriel Ebner and Sebastian Ullrich and Jared Roesch and Jeremy Avigad and Leonardo de Moura},
  year = {2017},
  doi = {10.1145/3110278},
  url = {http://doi.acm.org/10.1145/3110278},
  researchr = {https://researchr.org/publication/EbnerURAM17},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {1},
  number = {ICFP},
}

@inproceedings{SozeauT14,
  title = {Universe Polymorphism in Coq},
  author = {Matthieu Sozeau and Nicolas Tabareau},
  year = {2014},
  doi = {10.1007/978-3-319-08970-6_32},
  url = {http://dx.doi.org/10.1007/978-3-319-08970-6_32},
  researchr = {https://researchr.org/publication/SozeauT14},
  cites = {0},
  citedby = {0},
  pages = {499-514},
  booktitle = {Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings},
  editor = {Gerwin Klein and Ruben Gamboa},
  volume = {8558},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-08969-0},
}

@unpublished{Gundry2012,
  title = {A tutorial implementation of dynamic pattern unification: A dependently typed programming language implementation pearl},
  author = {Adam Gundry and Conor McBride},
  year = {2012},
  researchr = {https://researchr.org/publication/Gundry2012},
  cites = {0},
  citedby = {0},
}

@unpublished{Eisenberg2021,
  title = {An Existential Crisis Resolved: Type inference for first-class existential types },
  author = {Richard A. Eisenberg and  Guillaume Duboc and Stephanie Weirich and Daniel Lee},
  year = {2021},
  researchr = {https://researchr.org/publication/Eisenberg2021},
  cites = {0},
  citedby = {0},
}

@article{coquand1991algorithm,
  title = {An algorithm for testing conversion in type theory},
  author = {Coquand, Thierry},
  year = {1991},
  researchr = {https://researchr.org/publication/coquand1991algorithm},
  cites = {0},
  citedby = {0},
  journal = {Logical frameworks},
  volume = {1},
  pages = {255-279},
}

@article{DBLP:journals-corr-abs-1202-4905,
  title = {A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions},
  author = {Andrea Asperti and Wilmer Ricciotti and Claudio Sacerdoti Coen and Enrico Tassi},
  year = {2012},
  doi = {10.2168/LMCS-8(1:18)2012},
  url = {https://doi.org/10.2168/LMCS-8(1:18)2012},
  researchr = {https://researchr.org/publication/DBLP%3Ajournals-corr-abs-1202-4905},
  cites = {0},
  citedby = {0},
  journal = {Log. Methods Comput. Sci.},
  volume = {8},
  number = {1},
}

@article{SerranoHJV20,
  title = {A quick look at impredicativity},
  author = {Alejandro Serrano 0001 and Jurriaan Hage and Simon Peyton Jones and Dimitrios Vytiniotis},
  year = {2020},
  doi = {10.1145/3408971},
  url = {https://doi.org/10.1145/3408971},
  researchr = {https://researchr.org/publication/SerranoHJV20},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {ICFP},
}

@article{Pientka13,
  title = {An insider's look at LF type reconstruction: everything you (n)ever wanted to know},
  author = {Brigitte Pientka},
  year = {2013},
  doi = {10.1017/S0956796812000408},
  url = {http://dx.doi.org/10.1017/S0956796812000408},
  researchr = {https://researchr.org/publication/Pientka13},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {23},
  number = {1},
  pages = {1-37},
}

@inproceedings{StarkSK19,
  title = {Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions},
  author = {Kathrin Stark and Steven Schäfer and Jonas Kaiser},
  year = {2019},
  doi = {10.1145/3293880.3294101},
  url = {https://doi.org/10.1145/3293880.3294101},
  researchr = {https://researchr.org/publication/StarkSK19},
  cites = {0},
  citedby = {0},
  pages = {166-180},
  booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019},
  editor = {Assia Mahboubi and Magnus O. Myreen},
  publisher = {ACM},
  isbn = {978-1-4503-6222-1},
}

@article{CockxA20,
  title = {Elaborating dependent (co)pattern matching: No pattern left behind},
  author = {Jesper Cockx and Andreas Abel},
  year = {2020},
  doi = {10.1017/S0956796819000182},
  url = {https://doi.org/10.1017/S0956796819000182},
  researchr = {https://researchr.org/publication/CockxA20},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {30},
}

@inproceedings{KarachaliasSVJ15,
  title = {GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and laziness},
  author = {Georgios Karachalias and Tom Schrijvers and Dimitrios Vytiniotis and Simon L. Peyton Jones},
  year = {2015},
  doi = {10.1145/2784731.2784748},
  url = {http://doi.acm.org/10.1145/2784731.2784748},
  researchr = {https://researchr.org/publication/KarachaliasSVJ15},
  cites = {0},
  citedby = {0},
  pages = {424-436},
  booktitle = {Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015},
  editor = {Kathleen Fisher and John H. Reppy},
  publisher = {ACM},
  isbn = {978-1-4503-3669-7},
}

@article{DBLP:journals-corr-abs-2001-04301,
  title = {Tabled Typeclass Resolution},
  author = {Daniel Selsam and Sebastian Ullrich and Leonardo de Moura},
  year = {2020},
  url = {https://arxiv.org/abs/2001.04301},
  researchr = {https://researchr.org/publication/DBLP%3Ajournals-corr-abs-2001-04301},
  cites = {0},
  citedby = {0},
  journal = {CoRR},
  volume = {abs/2001.04301},
}

@article{Wiedijk02,
  title = {A New Implementation of Automath},
  author = {Freek Wiedijk},
  year = {2002},
  researchr = {https://researchr.org/publication/Wiedijk02},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {29},
  number = {3-4},
  pages = {365-387},
}

@inproceedings{SchaferTS15,
  title = {Autosubst: Reasoning with {de Bruijn} Terms and Parallel Substitutions},
  author = {Steven Schäfer and Tobias Tebbi and Gert Smolka},
  year = {2015},
  doi = {10.1007/978-3-319-22102-1_24},
  url = {http://dx.doi.org/10.1007/978-3-319-22102-1_24},
  researchr = {https://researchr.org/publication/SchaferTS15},
  cites = {0},
  citedby = {0},
  pages = {359-374},
  booktitle = {Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings},
  editor = {Christian Urban and Xingyuan Zhang},
  volume = {9236},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-22101-4},
}

@article{RouvoetAPKV20,
  title = {Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications},
  author = {Arjen Rouvoet and Hendrik van Antwerpen and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser},
  year = {2020},
  doi = {10.1145/3428248},
  url = {https://doi.org/10.1145/3428248},
  researchr = {https://researchr.org/publication/RouvoetAPKV20},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {OOPSLA},
}

@inproceedings{JuanD20,
  title = {Practical dependent type checking using twin types},
  author = {Víctor López Juan and Nils Anders Danielsson},
  year = {2020},
  doi = {10.1145/3406089.3409030},
  url = {https://doi.org/10.1145/3406089.3409030},
  researchr = {https://researchr.org/publication/JuanD20},
  cites = {0},
  citedby = {0},
  pages = {11-23},
  booktitle = {Proceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2020, Virtual Event, USA, August 23, 2020},
  editor = {James McKinna and Cyrus Omar},
  publisher = {ACM},
  isbn = {978-1-4503-8051-5},
}

@article{ChangBTB20,
  title = {Dependent type systems as macros},
  author = {Stephen Chang and Michael Ballantyne and Milo Turner and William J. Bowman},
  year = {2020},
  doi = {10.1145/3371071},
  url = {https://doi.org/10.1145/3371071},
  researchr = {https://researchr.org/publication/ChangBTB20},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {POPL},
}