publications:
- title: "Unification in Many-Sorted Algebras as a Device for Incremental Semantic Analysis"
  author:
  - name: "Gregor Snelting"
    link: "https://researchr.org/alias/gregor-snelting"
  - name: "Wolfgang Henhapl"
    link: "https://researchr.org/alias/wolfgang-henhapl"
  year: "1986"
  tags:
  - "analysis"
  - " algebra"
  - "incremental"
  researchr: "https://researchr.org/publication/SneltingH86"
  cites: 0
  citedby: 0
  pages: "229-235"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "SneltingH86"
- title: "Aspects of the Implementation of Type Theory"
  author:
  - name: "Robert W. Harper"
    link: "https://researchr.org/alias/robert-w.-harper"
  year: "1985"
  researchr: "https://researchr.org/publication/Har85-0"
  cites: 0
  citedby: 0
  school: "Cornell University"
  kind: "phdthesis"
  key: "Har85-0"
- title: "Optimizing Higher-Order Pattern Unification"
  author:
  - name: "Brigitte Pientka"
    link: "https://researchr.org/alias/brigitte-pientka"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "2003"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2741&spage=473"
  links:
    doi: "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:
  - name: "Franz Baader"
    link: "https://researchr.org/alias/franz-baader"
  volume: "2741"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-40559-3"
  kind: "inproceedings"
  key: "PientkaP03"
- title: "A role for dependent types in Haskell"
  author:
  - name: "Stephanie Weirich"
    link: "https://researchr.org/alias/stephanie-weirich"
  - name: "Pritam Choudhury"
    link: "https://researchr.org/alias/pritam-choudhury"
  - name: "Antoine Voizard"
    link: "https://researchr.org/alias/antoine-voizard"
  - name: "Richard A. Eisenberg"
    link: "https://researchr.org/alias/richard-a.-eisenberg"
  year: "2019"
  doi: "https://doi.org/10.1145/3341705"
  links:
    doi: "https://doi.org/10.1145/3341705"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/WeirichCVE19"
  researchr: "https://researchr.org/publication/WeirichCVE19"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "3"
  number: "ICFP"
  kind: "article"
  key: "WeirichCVE19"
- title: "Design and Implementation of the Andromeda Proof Assistant"
  author:
  - name: "Andrej Bauer"
    link: "https://researchr.org/alias/andrej-bauer"
  - name: "Gaëtan Gilbert"
    link: "https://researchr.org/alias/ga%C3%ABtan-gilbert"
  - name: "Philipp G. Haselwarter"
    link: "https://researchr.org/alias/philipp-g.-haselwarter"
  - name: "Matija Pretnar"
    link: "https://researchr.org/alias/matija-pretnar"
  - name: "Christopher A. Stone"
    link: "https://researchr.org/alias/christopher-a.-stone"
  year: "2016"
  doi: "https://doi.org/10.4230/LIPIcs.TYPES.2016.5"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.TYPES.2016.5"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/types/BauerGHPS16"
  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:
  - name: "Silvia Ghilezan"
    link: "https://researchr.org/alias/silvia-ghilezan"
  - name: "Herman Geuvers"
    link: "https://researchr.org/alias/herman-geuvers"
  - name: "Jelena Ivetic"
    link: "https://researchr.org/alias/jelena-ivetic"
  volume: "97"
  series: "LIPIcs"
  publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik"
  isbn: "978-3-95977-065-1"
  kind: "inproceedings"
  key: "BauerGHPS16"
- title: "Dependent ML An approach to practical programming with dependent types"
  author:
  - name: "Hongwei Xi"
    link: "https://researchr.org/alias/hongwei-xi"
  year: "2007"
  doi: "http://dx.doi.org/10.1017/S0956796806006216"
  links:
    doi: "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"
  kind: "article"
  key: "Xi07:0"
- title: "A compiled implementation of strong reduction"
  author:
  - name: "Benjamin Grégoire"
    link: "https://researchr.org/alias/benjamin-gr%C3%A9goire"
  - name: "Xavier Leroy"
    link: "http://pauillac.inria.fr/~xleroy/"
  year: "2002"
  doi: "http://doi.acm.org/10.1145/581478.581501"
  links:
    doi: "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)"
  kind: "inproceedings"
  key: "GregoireL02"
- title: "Elf: A Language for Logic Definition and Verified Metaprogramming"
  author:
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  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"
  kind: "inproceedings"
  key: "Pfenning89"
- title: "The New Rewriting Engine of Dedukti (System Description)"
  author:
  - name: "Gabriel Hondet"
    link: "https://researchr.org/alias/gabriel-hondet"
  - name: "Frédéric Blanqui"
    link: "https://researchr.org/alias/fr%C3%A9d%C3%A9ric-blanqui"
  year: "2020"
  doi: "https://doi.org/10.4230/LIPIcs.FSCD.2020.35"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.FSCD.2020.35"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fscd/HondetB20"
  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:
  - name: "Zena M. Ariola"
    link: "https://researchr.org/alias/zena-m.-ariola"
  volume: "167"
  series: "LIPIcs"
  publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik"
  isbn: "978-3-95977-155-9"
  kind: "inproceedings"
  key: "HondetB20"
- title: "RefinedRust: A Type System for High-Assurance Verification of Rust Programs"
  author:
  - name: "Lennard Gäher"
    link: "https://researchr.org/alias/lennard-g%C3%A4her"
  - name: "Michael Sammler"
    link: "https://researchr.org/alias/michael-sammler"
  - name: "Ralf Jung 0002"
    link: "https://researchr.org/alias/ralf-jung-0002"
  - name: "Robbert Krebbers"
    link: "https://researchr.org/alias/robbert-krebbers"
  - name: "Derek Dreyer"
    link: "https://researchr.org/alias/derek-dreyer"
  year: "2024"
  doi: "https://doi.org/10.1145/3656422"
  links:
    doi: "https://doi.org/10.1145/3656422"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/GaherSJKD24"
  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"
  kind: "article"
  key: "GaherSJKD24"
- title: "Small, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting"
  author:
  - name: "Michael Färber"
    link: "https://researchr.org/alias/michael-f%C3%A4rber"
  year: "2021"
  researchr: "https://researchr.org/publication/frber2021small"
  cites: 0
  citedby: 0
  kind: "misc"
  key: "frber2021small"
- title: "A dependently typed calculus with pattern matching and erasure inference"
  author:
  - name: "Matus Tejiscak"
    link: "https://researchr.org/alias/matus-tejiscak"
  year: "2020"
  doi: "https://doi.org/10.1145/3408973"
  links:
    doi: "https://doi.org/10.1145/3408973"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/Tejiscak20"
  researchr: "https://researchr.org/publication/Tejiscak20"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "4"
  number: "ICFP"
  kind: "article"
  key: "Tejiscak20"
- title: "Efficient rewriting using decision trees"
  author:
  - name: "Hondet, Gabriel"
    link: "https://researchr.org/alias/hondet%2C-gabriel"
  year: "2019"
  month: "Aug"
  links:
    "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"
  kind: "mastersthesis"
  key: "hondet:hal-02317471"
- title: "Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  year: "2019"
  doi: "https://doi.org/10.4230/LIPIcs.TYPES.2019.2"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.TYPES.2019.2"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/types/Cockx19"
  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:
  - name: "Marc Bezem"
    link: "https://researchr.org/alias/marc-bezem"
  - name: "Assia Mahboubi"
    link: "https://researchr.org/alias/assia-mahboubi"
  volume: "175"
  series: "LIPIcs"
  publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik"
  isbn: "978-3-95977-158-0"
  kind: "inproceedings"
  key: "Cockx19"
- title: "Congruence Closure in Intensional Type Theory"
  author:
  - name: "Daniel Selsam"
    link: "https://researchr.org/alias/daniel-selsam"
  - name: "Leonardo de Moura"
    link: "https://researchr.org/alias/leonardo-de-moura"
  year: "2016"
  doi: "http://dx.doi.org/10.1007/978-3-319-40229-1_8"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-40229-1_8"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cade/SelsamM16"
  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:
  - name: "Nicola Olivetti"
    link: "https://researchr.org/alias/nicola-olivetti"
  - name: "Ashish Tiwari"
    link: "https://researchr.org/alias/ashish-tiwari"
  volume: "9706"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-40228-4"
  kind: "inproceedings"
  key: "SelsamM16"
- title: "A Coverage Checking Algorithm for LF"
  author:
  - name: "Carsten Schürmann"
    link: "https://researchr.org/alias/carsten-sch%C3%BCrmann"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "2003"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=120"
  links:
    doi: "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:
  - name: "David A. Basin"
    link: "https://researchr.org/alias/david-a.-basin"
  - name: "Burkhart Wolff"
    link: "https://researchr.org/alias/burkhart-wolff"
  volume: "2758"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-40664-6"
  kind: "inproceedings"
  key: "SchurmannP03"
- title: "Equations reloaded: high-level dependently-typed functional programming and proving in Coq"
  author:
  - name: "Matthieu Sozeau"
    link: "https://researchr.org/alias/matthieu-sozeau"
  - name: "Cyprien Mangin"
    link: "https://researchr.org/alias/cyprien-mangin"
  year: "2019"
  doi: "https://doi.org/10.1145/3341690"
  links:
    doi: "https://doi.org/10.1145/3341690"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/SozeauM19"
  researchr: "https://researchr.org/publication/SozeauM19"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "3"
  number: "ICFP"
  kind: "article"
  key: "SozeauM19"
- title: "Elaborator reflection: extending Idris in Idris"
  author:
  - name: "David Christiansen"
    link: "https://researchr.org/alias/david-christiansen"
  - name: "Edwin Brady"
    link: "http://www.cs.st-andrews.ac.uk/~eb"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2951913.2951932"
  links:
    doi: "http://doi.acm.org/10.1145/2951913.2951932"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/ChristiansenB16"
  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:
  - name: "Jacques Garrigue"
    link: "https://researchr.org/alias/jacques-garrigue"
  - name: "Gabriele Keller"
    link: "https://researchr.org/alias/gabriele-keller"
  - name: "Eijiro Sumii"
    link: "https://researchr.org/alias/eijiro-sumii"
  publisher: "ACM"
  isbn: "978-1-4503-4219-3"
  kind: "inproceedings"
  key: "ChristiansenB16"
- title: "The Lean Theorem Prover (System Description)"
  author:
  - name: "Leonardo Mendonça de Moura"
    link: "https://researchr.org/alias/leonardo-mendon%C3%A7a-de-moura"
  - name: "Soonho Kong"
    link: "https://researchr.org/alias/soonho-kong"
  - name: "Jeremy Avigad"
    link: "https://researchr.org/alias/jeremy-avigad"
  - name: "Floris van Doorn"
    link: "https://researchr.org/alias/floris-van-doorn"
  - name: "Jakob von Raumer"
    link: "https://researchr.org/alias/jakob-von-raumer"
  year: "2015"
  doi: "http://dx.doi.org/10.1007/978-3-319-21401-6_26"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-21401-6_26"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cade/MouraKADR15"
  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:
  - name: "Amy P. Felty"
    link: "https://researchr.org/alias/amy-p.-felty"
  - name: "Aart Middeldorp"
    link: "https://researchr.org/alias/aart-middeldorp"
  volume: "9195"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-21400-9"
  kind: "inproceedings"
  key: "MouraKADR15"
- title: "Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection"
  author:
  - name: "David Raymond Christiansen"
    link: "https://researchr.org/alias/david-raymond-christiansen"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2746325.2746326"
  links:
    doi: "http://doi.acm.org/10.1145/2746325.2746326"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ifl/Christiansen14"
  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:
  - name: "Sam Tobin-Hochstadt"
    link: "https://researchr.org/alias/sam-tobin-hochstadt"
  publisher: "ACM"
  isbn: "978-1-4503-3284-2"
  kind: "inproceedings"
  key: "Christiansen14-1"
- title: "Towards a practical programming language based on dependent type theory"
  author:
  - name: "Ulf Norell"
    link: "https://researchr.org/alias/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"
  kind: "phdthesis"
  key: "Norell2007towardsapractical"
- title: "Dependent Types in Practical Programming"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "1999"
  doi: "http://doi.acm.org/10.1145/292540.292560"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "XiP99"
- title: "ELPI: Fast, Embeddable, \\lambda Prolog Interpreter"
  author:
  - name: "Cvetan Dunchev"
    link: "https://researchr.org/alias/cvetan-dunchev"
  - name: "Ferruccio Guidi"
    link: "https://researchr.org/alias/ferruccio-guidi"
  - name: "Claudio Sacerdoti Coen"
    link: "https://researchr.org/alias/claudio-sacerdoti-coen"
  - name: "Enrico Tassi"
    link: "https://researchr.org/alias/enrico-tassi"
  year: "2015"
  doi: "http://dx.doi.org/10.1007/978-3-662-48899-7_32"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-662-48899-7_32"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lpar/DunchevGCT15"
  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:
  - name: "Martin Davis"
    link: "https://researchr.org/alias/martin-davis"
  - name: "Ansgar Fehnker"
    link: "https://researchr.org/alias/ansgar-fehnker"
  - name: "Annabelle McIver"
    link: "https://researchr.org/alias/annabelle-mciver"
  - name: "Andrei Voronkov"
    link: "https://researchr.org/alias/andrei-voronkov"
  volume: "9450"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-662-48898-0"
  kind: "inproceedings"
  key: "DunchevGCT15"
- title: "Elaborating Inductive Definitions"
  author:
  - name: "Pierre-Evariste Dagand"
    link: "https://researchr.org/alias/pierre-evariste-dagand"
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  year: "2012"
  researchr: "https://researchr.org/publication/dagand2012elaborating"
  cites: 0
  citedby: 0
  kind: "misc"
  key: "dagand2012elaborating"
- title: "Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages"
  author:
  - name: "Sebastian Ullrich"
    link: "https://pp.ipd.kit.edu/~ullrich/?lang=en"
  - name: "Leonardo de Moura"
    link: "https://researchr.org/alias/leonardo-de-moura"
  year: "2020"
  doi: "https://doi.org/10.1007/978-3-030-51054-1_10"
  links:
    doi: "https://doi.org/10.1007/978-3-030-51054-1_10"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cade/0002M20"
  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:
  - name: "Nicolas Peltier"
    link: "https://researchr.org/alias/nicolas-peltier"
  - name: "Viorica Sofronie-Stokkermans"
    link: "https://researchr.org/alias/viorica-sofronie-stokkermans"
  volume: "12167"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-030-51054-1"
  kind: "inproceedings"
  key: "0002M20-2"
- title: "The Little Typer"
  author:
  - name: "Friedman, Daniel P"
    link: "https://researchr.org/alias/friedman%2C-daniel-p"
  - name: "Christiansen, David Thrane"
    link: "https://researchr.org/alias/christiansen%2C-david-thrane"
  year: "2018"
  researchr: "https://researchr.org/publication/friedman2018little"
  cites: 0
  citedby: 0
  publisher: "MIT Press"
  kind: "book"
  key: "friedman2018little"
- title: "Implementation Techniques for Inductive Types in Plastic"
  author:
  - name: "Paul Callaghan"
    link: "https://researchr.org/alias/paul-callaghan"
  - name: "Zhaohui Luo"
    link: "https://researchr.org/alias/zhaohui-luo"
  year: "1999"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1956/19560094.htm"
  links:
    doi: "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:
  - name: "Thierry Coquand"
    link: "https://researchr.org/alias/thierry-coquand"
  - name: "Peter Dybjer"
    link: "https://researchr.org/alias/peter-dybjer"
  - name: "Bengt Nordström"
    link: "https://researchr.org/alias/bengt-nordstr%C3%B6m"
  - name: "Jan M. Smith"
    link: "https://researchr.org/alias/jan-m.-smith"
  volume: "1956"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-41517-3"
  kind: "inproceedings"
  key: "CallaghanL99"
- title: "alpha-Prolog: A Logic Programming Language with Names, Binding and a-Equivalence"
  author:
  - name: "James Cheney"
    link: "https://researchr.org/alias/james-cheney"
  - name: "Christian Urban"
    link: "https://researchr.org/alias/christian-urban"
  year: "2004"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3132&spage=269"
  links:
    doi: "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:
  - name: "Bart Demoen"
    link: "https://researchr.org/alias/bart-demoen"
  - name: "Vladimir Lifschitz"
    link: "https://researchr.org/alias/vladimir-lifschitz"
  volume: "3132"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-22671-0"
  kind: "inproceedings"
  key: "CheneyU04"
- title: "Executable Specification of Static Semantics"
  author:
  - name: "Thierry Despeyroux"
    link: "https://researchr.org/alias/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:
  - name: "Gilles Kahn"
    link: "https://researchr.org/alias/gilles-kahn"
  - name: "David B. MacQueen"
    link: "https://researchr.org/alias/david-b.-macqueen"
  - name: "Gordon D. Plotkin"
    link: "https://researchr.org/alias/gordon-d.-plotkin"
  volume: "173"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-13346-1"
  kind: "inproceedings"
  key: "Despeyroux84"
- title: "A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance"
  author:
  - name: "Andreas Abel"
    link: "https://researchr.org/alias/andreas-abel"
  - name: "Thierry Coquand"
    link: "https://researchr.org/alias/thierry-coquand"
  - name: "Miguel Pagano"
    link: "https://researchr.org/alias/miguel-pagano"
  year: "2009"
  doi: "http://dx.doi.org/10.1007/978-3-642-02273-9_3"
  links:
    doi: "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:
  - name: "Pierre-Louis Curien"
    link: "https://researchr.org/alias/pierre-louis-curien"
  volume: "5608"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-02272-2"
  kind: "inproceedings"
  key: "AbelCP09"
- title: "User Interaction with the Matita Proof Assistant"
  author:
  - name: "Andrea Asperti"
    link: "https://researchr.org/alias/andrea-asperti"
  - name: "Claudio Sacerdoti Coen"
    link: "https://researchr.org/alias/claudio-sacerdoti-coen"
  - name: "Enrico Tassi"
    link: "https://researchr.org/alias/enrico-tassi"
  - name: "Stefano Zacchiroli"
    link: "https://researchr.org/alias/stefano-zacchiroli"
  year: "2007"
  doi: "http://dx.doi.org/10.1007/s10817-007-9070-5"
  links:
    doi: "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"
  kind: "article"
  key: "AspertiCTZ07"
- title: "Practical implementation of a dependently typed functional programming language"
  author:
  - name: "Edwin Brady"
    link: "http://www.cs.st-andrews.ac.uk/~eb"
  year: "2005"
  doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.417649"
  note: "British Library, EThOS"
  links:
    doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.417649"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/ethos/Brady05"
  researchr: "https://researchr.org/publication/ethos-4985"
  cites: 0
  citedby: 0
  school: "Durham University, UK"
  kind: "phdthesis"
  key: "ethos-4985"
- title: "Type checking through unification"
  author:
  - name: "Francesco Mazzoli"
    link: "https://researchr.org/alias/francesco-mazzoli"
  - name: "Andreas Abel"
    link: "https://researchr.org/alias/andreas-abel"
  year: "2016"
  researchr: "https://researchr.org/publication/mazzoli2016type"
  cites: 0
  citedby: 0
  kind: "unpublished"
  key: "mazzoli2016type"
- title: "System Description: Twelf - A Meta-Logical Framework for Deductive Systems"
  author:
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  - name: "Carsten Schürmann"
    link: "https://researchr.org/alias/carsten-sch%C3%BCrmann"
  year: "1999"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1632/16320202.htm"
  links:
    doi: "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:
  - name: "Harald Ganzinger"
    link: "https://researchr.org/alias/harald-ganzinger"
  volume: "1632"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-66222-7"
  kind: "inproceedings"
  key: "PfenningS99"
- title: "Growing a proof assistant"
  author:
  - name: "Bowman, William J"
    link: "https://researchr.org/alias/bowman%2C-william-j"
  year: "2016"
  researchr: "https://researchr.org/publication/bowman2016growing"
  cites: 0
  citedby: 0
  journal: "Higher-Order Programming with Effects"
  volume: "65"
  kind: "article"
  key: "bowman2016growing"
- title: "Elaboration in Dependent Type Theory"
  author:
  - name: "Leonardo Mendon{\\c{c}}a de Moura"
    link: "https://researchr.org/alias/leonardo-mendon%7B%5Ebc%7Bc%7D%7Da-de-moura"
  - name: "Jeremy Avigad"
    link: "https://researchr.org/alias/jeremy-avigad"
  - name: "Soonho Kong"
    link: "https://researchr.org/alias/soonho-kong"
  - name: "Cody Roux"
    link: "https://researchr.org/alias/cody-roux"
  year: "2015"
  links:
    "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"
  kind: "article"
  key: "DBLP:journals-corr-MouraAKR15"
- title: "Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting"
  author:
  - name: "Michael Färber"
    link: "https://researchr.org/alias/michael-f%C3%A4rber"
  year: "2022"
  doi: "https://doi.org/10.1145/3497775.3503683"
  links:
    doi: "https://doi.org/10.1145/3497775.3503683"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/Farber22"
  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:
  - name: "Andrei Popescu 0001"
    link: "https://researchr.org/alias/andrei-popescu-0001"
  - name: "Steve Zdancewic"
    link: "https://researchr.org/alias/steve-zdancewic"
  publisher: "ACM"
  isbn: "978-1-4503-9182-5"
  kind: "inproceedings"
  key: "Farber22"
- title: "The PSG System: From Formal Language Definitions to Interactive Programming Environments"
  author:
  - name: "Rolf Bahlke"
    link: "https://researchr.org/alias/rolf-bahlke"
  - name: "Gregor Snelting"
    link: "https://researchr.org/alias/gregor-snelting"
  year: "1986"
  doi: "http://doi.acm.org/10.1145/6465.20890"
  links:
    doi: "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"
  kind: "article"
  key: "BahlkeS86:0"
- title: "Type inference, Haskell and dependent types"
  author:
  - name: "Adam Michael Gundry"
    link: "https://researchr.org/alias/adam-michael-gundry"
  year: "2013"
  doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.605927"
  note: "British Library, EThOS"
  links:
    doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.605927"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/ethos/Gundry13"
  researchr: "https://researchr.org/publication/ethos-1465"
  cites: 0
  citedby: 0
  school: "University of Strathclyde, Glasgow, UK"
  kind: "phdthesis"
  key: "ethos-1465"
- title: "Unnesting of Copatterns"
  author:
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Brigitte Pientka"
    link: "https://researchr.org/alias/brigitte-pientka"
  - name: "David Thibodeau"
    link: "https://researchr.org/alias/david-thibodeau"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-319-08918-8_3"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-08918-8_3"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/rta/Setzer0PT14"
  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:
  - name: "Gilles Dowek"
    link: "https://researchr.org/alias/gilles-dowek"
  volume: "8560"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-08917-1"
  kind: "inproceedings"
  key: "Setzer0PT14"
- title: "MiniAgda: Integrating Sized and Dependent Types"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  year: "2010"
  doi: "http://www.easychair.org/publications/?page=506004245"
  links:
    doi: "http://www.easychair.org/publications/?page=506004245"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/000110"
  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:
  - name: "Ekaterina Komendantskaya"
    link: "https://researchr.org/alias/ekaterina-komendantskaya"
  - name: "Ana Bove"
    link: "https://researchr.org/alias/ana-bove"
  - name: "Milad Niqui"
    link: "https://researchr.org/alias/milad-niqui"
  volume: "5"
  series: "EPiC Series"
  publisher: "EasyChair"
  kind: "inproceedings"
  key: "000110-2"
- title: "Mode and Termination Checking for Higher-Order Logic Programs"
  author:
  - name: "Ekkehard Rohwedder"
    link: "https://researchr.org/alias/ekkehard-rohwedder"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  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:
  - name: "Hanne Riis Nielson"
    link: "https://researchr.org/alias/hanne-riis-nielson"
  volume: "1058"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-61055-3"
  kind: "inproceedings"
  key: "RohwedderP96"
- title: "Epigram reloaded: a standalone typechecker for ETT"
  author:
  - name: "James Chapman"
    link: "https://researchr.org/alias/james-chapman"
  - name: "Thorsten Altenkirch"
    link: "http://www.cs.nott.ac.uk/~txa"
  - name: "Conor McBride"
    link: "http://personal.cis.strath.ac.uk/~conor/"
  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:
  - name: "Marko C. J. D. van Eekelen"
    link: "https://researchr.org/alias/marko-c.-j.-d.-van-eekelen"
  volume: "6"
  series: "Trends in Functional Programming"
  publisher: "Intellect"
  isbn: "978-1-84150-176-5"
  kind: "inproceedings"
  key: "ChapmanAM05"
- title: "The theory of LEGO"
  author:
  - name: "Robert Pollack"
    link: "https://researchr.org/alias/robert-pollack"
  year: "1995"
  doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.561652"
  note: "British Library, EThOS"
  links:
    doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.561652"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/ethos/Pollack95"
  researchr: "https://researchr.org/publication/ethos-7403"
  cites: 0
  citedby: 0
  kind: "phdthesis"
  key: "ethos-7403"
- title: "Functional pearl: I am not a number-I am a free variable"
  author:
  - name: "Conor McBride"
    link: "http://personal.cis.strath.ac.uk/~conor/"
  - name: "James McKinna"
    link: "https://researchr.org/alias/james-mckinna"
  year: "2004"
  doi: "http://doi.acm.org/10.1145/1017472.1017477"
  links:
    doi: "http://doi.acm.org/10.1145/1017472.1017477"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/haskell/McBrideM04"
  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:
  - name: "Henrik Nilsson"
    link: "https://researchr.org/alias/henrik-nilsson"
  publisher: "ACM"
  kind: "inproceedings"
  key: "McBrideM04-0"
- title: "Elaboration with first-class implicit function types"
  author:
  - name: "András Kovács"
    link: "https://researchr.org/alias/andr%C3%A1s-kov%C3%A1cs"
  year: "2020"
  doi: "https://doi.org/10.1145/3408983"
  links:
    doi: "https://doi.org/10.1145/3408983"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/Kovacs20"
  researchr: "https://researchr.org/publication/Kovacs20"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "4"
  number: "ICFP"
  kind: "article"
  key: "Kovacs20"
- title: "An Algorithm for Type-Checking Dependent Types"
  author:
  - name: "Thierry Coquand"
    link: "https://researchr.org/alias/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"
  kind: "article"
  key: "Coquand96"
- 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:
  - name: "Ronan Saillard"
    link: "https://researchr.org/alias/ronan-saillard"
  year: "2015"
  doi: "https://tel.archives-ouvertes.fr/tel-01299180"
  links:
    doi: "https://tel.archives-ouvertes.fr/tel-01299180"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/hal/Saillard15a"
  researchr: "https://researchr.org/publication/hal-8150"
  cites: 0
  citedby: 0
  school: "Mines ParisTech, France"
  kind: "phdthesis"
  key: "hal-8150"
- title: "Implementing type theory in higher order constraint logic programming"
  author:
  - name: "Ferruccio Guidi"
    link: "https://researchr.org/alias/ferruccio-guidi"
  - name: "Claudio Sacerdoti Coen"
    link: "https://researchr.org/alias/claudio-sacerdoti-coen"
  - name: "Enrico Tassi"
    link: "https://researchr.org/alias/enrico-tassi"
  year: "2019"
  doi: "https://doi.org/10.1017/S0960129518000427"
  links:
    doi: "https://doi.org/10.1017/S0960129518000427"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/mscs/GuidiCT19"
  researchr: "https://researchr.org/publication/GuidiCT19"
  cites: 0
  citedby: 0
  journal: "Mathematical Structures in Computer Science"
  volume: "29"
  number: "8"
  pages: "1125-1150"
  kind: "article"
  key: "GuidiCT19"
- title: "Implementing a modal dependent type theory"
  author:
  - name: "Daniel Gratzer"
    link: "https://researchr.org/alias/daniel-gratzer"
  - name: "Jonathan Sterling"
    link: "https://researchr.org/alias/jonathan-sterling"
  - name: "Lars Birkedal"
    link: "https://researchr.org/alias/lars-birkedal"
  year: "2019"
  doi: "https://doi.org/10.1145/3341711"
  links:
    doi: "https://doi.org/10.1145/3341711"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/GratzerSB19"
  researchr: "https://researchr.org/publication/GratzerSB19"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "3"
  number: "ICFP"
  kind: "article"
  key: "GratzerSB19"
- title: "OutsideIn(X) Modular type inference with local assumptions"
  author:
  - name: "Dimitrios Vytiniotis"
    link: "http://"
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  - name: "Tom Schrijvers"
    link: "http://users.ugent.be/~tschrijv"
  - name: "Martin Sulzmann"
    link: "https://researchr.org/alias/martin-sulzmann"
  year: "2011"
  abstract: " Advanced type system features, such as GADTs, type classes and type families, have proven to be invaluable language extensions for ensuring data invariants and program correctness. Unfortunately, they pose a tough problem for type inference when they are used as local type assumptions. Local type assumptions often result in the lack of principal types and cast the generalisation of local let-bindings prohibitively difficult to implement and specify. User-declared axioms only make this situation worse. In this paper, we explain the problems and – perhaps controversially – argue for abandoning local let-binding generalisation. We give empirical results that local let generalisation is only sporadically used by Haskell programmers. Moving on, we present a novel constraint-based type inference approach for local type assumptions. Our system, called OutsideIn(X), is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm. OutsideIn(X) extends the constraints of X by introducing implication constraints on top. We describe the strategy for solving these implication constraints, which, in turn, relies on a constraint solver for X. We characterise the properties of the constraint solver for X so that the resulting algorithm only accepts programs with principal types, even when the type system specification accepts programs that do not enjoy principal types. Going beyond the general framework, we give a particular constraint solver for X = type classes + GADTs + type families, a non-trivial challenge in its own right. This constraint solver has been implemented and distributed as part of GHC 7."
  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"
  kind: "article"
  key: "VytiniotisJSS11"
- title: "Type checking in the presence of meta-variables"
  author:
  - name: "Norell, Ulf"
    link: "https://researchr.org/alias/norell%2C-ulf"
  - name: "Coquand, Catarina"
    link: "https://researchr.org/alias/coquand%2C-catarina"
  year: "2007"
  researchr: "https://researchr.org/publication/norell2007type"
  cites: 0
  citedby: 0
  kind: "article"
  key: "norell2007type"
- title: "Crafting a Proof Assistant"
  author:
  - name: "Andrea Asperti"
    link: "https://researchr.org/alias/andrea-asperti"
  - name: "Claudio Sacerdoti Coen"
    link: "https://researchr.org/alias/claudio-sacerdoti-coen"
  - name: "Enrico Tassi"
    link: "https://researchr.org/alias/enrico-tassi"
  - name: "Stefano Zacchiroli"
    link: "https://researchr.org/alias/stefano-zacchiroli"
  year: "2006"
  doi: "http://dx.doi.org/10.1007/978-3-540-74464-1_2"
  links:
    doi: "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:
  - name: "Thorsten Altenkirch"
    link: "http://www.cs.nott.ac.uk/~txa"
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  volume: "4502"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-540-74463-4"
  kind: "inproceedings"
  key: "AspertiCTZ06"
- title: "Algorithms for Equality and Unification in the Presence of Notational Definitions"
  author:
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  - name: "Carsten Schürmann"
    link: "https://researchr.org/alias/carsten-sch%C3%BCrmann"
  year: "1998"
  doi: "http://www.elsevier.com/gej-ng/31/29/23/41/23/show/Products/notes/index.htt#006"
  links:
    doi: "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"
  kind: "article"
  key: "PfenningS98"
- title: "Idris 2: Quantitative Type Theory in Action"
  author:
  - name: "Edwin Brady"
    link: "https://researchr.org/alias/edwin-brady"
  year: "2021"
  researchr: "https://researchr.org/publication/Brady2021"
  cites: 0
  citedby: 0
  kind: "unpublished"
  key: "Brady2021"
- title: "A compact kernel for the calculus of inductive constructions"
  author:
  - name: "A. Asperti"
    link: "https://researchr.org/alias/a.-asperti"
  - name: " W. Ricciotti"
    link: "https://researchr.org/alias/w.-ricciotti"
  - name: " Coen Sacerdoti"
    link: "https://researchr.org/alias/coen-sacerdoti"
  - name: "E. Tassi"
    link: "https://researchr.org/alias/e.-tassi"
  year: "2009"
  doi: "10.1007/s12046-009-0003-3"
  researchr: "https://researchr.org/publication/Asperti2009"
  cites: 0
  citedby: 0
  kind: "article"
  key: "Asperti2009"
- title: "Hints in Unification"
  author:
  - name: "Andrea Asperti"
    link: "https://researchr.org/alias/andrea-asperti"
  - name: "Wilmer Ricciotti"
    link: "https://researchr.org/alias/wilmer-ricciotti"
  - name: "Claudio Sacerdoti Coen"
    link: "https://researchr.org/alias/claudio-sacerdoti-coen"
  - name: "Enrico Tassi"
    link: "https://researchr.org/alias/enrico-tassi"
  year: "2009"
  doi: "http://dx.doi.org/10.1007/978-3-642-03359-9_8"
  links:
    doi: "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:
  - name: "Stefan Berghofer"
    link: "https://researchr.org/alias/stefan-berghofer"
  - name: "Tobias Nipkow"
    link: "https://researchr.org/alias/tobias-nipkow"
  - name: "Christian Urban"
    link: "https://researchr.org/alias/christian-urban"
  - name: "Makarius Wenzel"
    link: "https://researchr.org/alias/makarius-wenzel"
  volume: "5674"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-03358-2"
  kind: "inproceedings"
  key: "AspertiRCT09"
- title: "Local type inference"
  author:
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  - name: "David N. Turner"
    link: "https://researchr.org/alias/david-n.-turner"
  year: "2000"
  doi: "http://doi.acm.org/10.1145/345099.345100"
  abstract: "We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. Both methods are local in the sense that missing annotations are recovered using only information from adjacent nodes in the syntax tree, without long-distance constraints such as unification variables. One method infers type arguments in polymorphic applications using a local constraint solver. The other infers annotations on bound variables in function abstractions by propagating type constraints downward from enclosing application nodes. We motivate our design choices by a statistical analysis of the uses of type inference in a sizable body of existing ML code."
  links:
    doi: "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"
  kind: "article"
  key: "PierceT-TOPLAS-2000"
- title: "The Lean 4 Theorem Prover and Programming Language"
  author:
  - name: "Leonardo de Moura"
    link: "https://researchr.org/alias/leonardo-de-moura"
  - name: "Sebastian Ullrich"
    link: "https://pp.ipd.kit.edu/~ullrich/?lang=en"
  year: "2021"
  doi: "https://doi.org/10.1007/978-3-030-79876-5_37"
  links:
    doi: "https://doi.org/10.1007/978-3-030-79876-5_37"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cade/Moura021"
  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:
  - name: "André Platzer"
    link: "https://researchr.org/alias/andr%C3%A9-platzer"
  - name: "Geoff Sutcliffe"
    link: "https://researchr.org/alias/geoff-sutcliffe"
  volume: "12699"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-030-79876-5"
  kind: "inproceedings"
  key: "Moura021"
- title: "Programming up to Congruence"
  author:
  - name: "Vilhelm Sjöberg"
    link: "https://researchr.org/alias/vilhelm-sj%C3%B6berg"
  - name: "Stephanie Weirich"
    link: "https://researchr.org/alias/stephanie-weirich"
  year: "2015"
  doi: "http://doi.acm.org/10.1145/2676726.2676974"
  links:
    doi: "http://doi.acm.org/10.1145/2676726.2676974"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/SjobergW15"
  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:
  - name: "Sriram K. Rajamani"
    link: "https://researchr.org/alias/sriram-k.-rajamani"
  - name: "David Walker"
    link: "https://researchr.org/alias/david-walker"
  publisher: "ACM"
  isbn: "978-1-4503-3300-9"
  kind: "inproceedings"
  key: "SjobergW15"
- title: "Bidirectional Elaboration of Dependently Typed Programs"
  author:
  - name: "Francisco Ferreira"
    link: "https://researchr.org/alias/francisco-ferreira"
  - name: "Brigitte Pientka"
    link: "https://researchr.org/alias/brigitte-pientka"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2643135.2643153"
  links:
    doi: "http://doi.acm.org/10.1145/2643135.2643153"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/FerreiraP14"
  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:
  - name: "Olaf Chitil"
    link: "https://researchr.org/alias/olaf-chitil"
  - name: "Andy King"
    link: "https://researchr.org/alias/andy-king"
  - name: "Olivier Danvy"
    link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/"
  publisher: "ACM"
  isbn: "978-1-4503-2947-7"
  kind: "inproceedings"
  key: "FerreiraP14-3"
- title: "The Constructive Engine"
  author:
  - name: "Gérard Huet"
    link: "https://researchr.org/alias/g%C3%A9rard-huet"
  year: "1989"
  doi: "http://dx.doi.org/10.1142/9789814368452_0004"
  links:
    doi: "http://dx.doi.org/10.1142/9789814368452_0004"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/series/wsscs/Huet89"
  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:
  - name: "R. Narasimhan"
    link: "https://researchr.org/alias/r.-narasimhan"
  volume: "16"
  series: "World Scientific Series in Computer Science"
  publisher: "World Scientific"
  isbn: "978-981-4507-35-6"
  kind: "incollection"
  key: "Huet89"
- title: "Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming"
  author:
  - name: "Sebastian Ullrich"
    link: "https://pp.ipd.kit.edu/~ullrich/?lang=en"
  - name: "Leonardo de Moura"
    link: "https://researchr.org/alias/leonardo-de-moura"
  year: "2019"
  links:
    "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"
  kind: "article"
  key: "DBLP:journals-corr-abs-1908-05647"
- title: "Inductive Families Need Not Store Their Indices"
  author:
  - name: "Edwin Brady"
    link: "http://www.cs.st-andrews.ac.uk/~eb"
  - name: "Conor McBride"
    link: "http://personal.cis.strath.ac.uk/~conor/"
  - name: "James McKinna"
    link: "https://researchr.org/alias/james-mckinna"
  year: "2003"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3085&spage=115"
  links:
    doi: "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:
  - name: "Stefano Berardi"
    link: "https://researchr.org/alias/stefano-berardi"
  - name: "Mario Coppo"
    link: "https://researchr.org/alias/mario-coppo"
  - name: "Ferruccio Damiani"
    link: "https://researchr.org/alias/ferruccio-damiani"
  volume: "3085"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-22164-6"
  kind: "inproceedings"
  key: "BradyMM03"
- title: "A simple type-theoretic language: Mini-TT"
  author:
  - name: "Thierry Coquand"
    link: "https://researchr.org/alias/thierry-coquand"
  - name: "Yoshiki Kinoshita"
    link: "https://researchr.org/alias/yoshiki-kinoshita"
  - name: "Bengt Nordström"
    link: "https://researchr.org/alias/bengt-nordstr%C3%B6m"
  - name: "Makoto Takeyama"
    link: "https://researchr.org/alias/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"
  kind: "article"
  key: "coquand2009simple"
- title: "Nonuniform Coercions via Unification Hints"
  author:
  - name: "Sacerdoti Coen, Claudio"
    link: "https://researchr.org/alias/sacerdoti-coen%2C-claudio"
  - name: "Tassi, Enrico"
    link: "https://researchr.org/alias/tassi%2C-enrico"
  year: "2011"
  month: "Mar"
  doi: "10.4204/eptcs.53.2"
  links:
    "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"
  kind: "article"
  key: "SacerdotiCoen2011"
- title: "A Tutorial Implementation of a Dependently Typed Lambda Calculus"
  author:
  - name: "Andres Löh"
    link: "https://researchr.org/alias/andres-l%C3%B6h"
  - name: "Conor McBride"
    link: "http://personal.cis.strath.ac.uk/~conor/"
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  year: "2010"
  doi: "http://dx.doi.org/10.3233/FI-2010-304"
  links:
    doi: "http://dx.doi.org/10.3233/FI-2010-304"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/fuin/LohMS10"
  researchr: "https://researchr.org/publication/LohMS10"
  cites: 0
  citedby: 0
  journal: "Fundamenta Informaticae"
  volume: "102"
  number: "2"
  pages: "177-207"
  kind: "article"
  key: "LohMS10"
- title: "Idris, a general-purpose dependently typed programming language: Design and implementation"
  author:
  - name: "Edwin Brady"
    link: "http://www.cs.st-andrews.ac.uk/~eb"
  year: "2013"
  doi: "http://dx.doi.org/10.1017/S095679681300018X"
  links:
    doi: "http://dx.doi.org/10.1017/S095679681300018X"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/Brady13"
  researchr: "https://researchr.org/publication/Brady13-Idris"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "23"
  number: "5"
  pages: "552-593"
  kind: "article"
  key: "Brady13-Idris"
- title: "Checking Algorithms for Pure Type Systems"
  author:
  - name: "L. S. van Benthem Jutting"
    link: "https://researchr.org/alias/l.-s.-van-benthem-jutting"
  - name: "James McKinna"
    link: "https://researchr.org/alias/james-mckinna"
  - name: "Robert Pollack"
    link: "https://researchr.org/alias/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:
  - name: "Henk Barendregt"
    link: "https://researchr.org/alias/henk-barendregt"
  - name: "Tobias Nipkow"
    link: "https://researchr.org/alias/tobias-nipkow"
  volume: "806"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-58085-9"
  kind: "inproceedings"
  key: "JuttingMP93"
- title: "A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading"
  author:
  - name: "Beta Ziliani"
    link: "https://researchr.org/alias/beta-ziliani"
  - name: "Matthieu Sozeau"
    link: "https://researchr.org/alias/matthieu-sozeau"
  year: "2017"
  doi: "http://dx.doi.org/10.1017/S0956796817000028"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796817000028"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/ZilianiS17"
  researchr: "https://researchr.org/publication/ZilianiS17"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "27"
  kind: "article"
  key: "ZilianiS17"
- title: "RefinedC: automating the foundational verification of C code with refined ownership types"
  author:
  - name: "Michael Sammler"
    link: "https://researchr.org/alias/michael-sammler"
  - name: "Rodolphe Lepigre"
    link: "https://researchr.org/alias/rodolphe-lepigre"
  - name: "Robbert Krebbers"
    link: "https://researchr.org/alias/robbert-krebbers"
  - name: "Kayvan Memarian"
    link: "https://researchr.org/alias/kayvan-memarian"
  - name: "Derek Dreyer"
    link: "https://researchr.org/alias/derek-dreyer"
  - name: "Deepak Garg 0001"
    link: "https://researchr.org/alias/deepak-garg-0001"
  year: "2021"
  doi: "https://doi.org/10.1145/3453483.3454036"
  links:
    doi: "https://doi.org/10.1145/3453483.3454036"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pldi/SammlerLKMD021"
  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:
  - name: "Stephen N. Freund"
    link: "https://researchr.org/alias/stephen-n.-freund"
  - name: "Eran Yahav"
    link: "https://researchr.org/alias/eran-yahav"
  publisher: "ACM"
  isbn: "978-1-4503-8391-2"
  kind: "inproceedings"
  key: "SammlerLKMD021"
- title: "TinkerType: a language for playing with formal systems"
  author:
  - name: "Michael Y. Levin"
    link: "https://researchr.org/alias/michael-y.-levin"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  year: "2003"
  doi: "http://dx.doi.org/10.1017/S0956796802004550"
  abstract: "TinkerType is a pragmatic framework for compact and modular description of formal systems (type systems, operational semantics, logics, etc.). A family of related systems is broken down into a set of clauses – individual inference rules – and a set of features controlling the inclusion of clauses in particular systems. Simple static checks are used to help maintain consistency of the generated systems. We present TinkerType and its implementation and describe its application to two substantial repositories of typed lambda-calculi. The first repository covers a broad range of typing features, including subtyping, polymorphism, type operators and kinding, computational effects, and dependent types. It describes both declarative and algorithmic aspects of the systems, and can be used with our tool, the TinkerType Assembler, to generate calculi either in the form of typeset collections of inference rules or as executable ML typecheckers. The second repository addresses a smaller collection of systems, and provides modularized proofs of basic safety properties."
  links:
    doi: "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"
  kind: "article"
  key: "LevinP03"
- title: "A metaprogramming framework for formal verification"
  author:
  - name: "Gabriel Ebner"
    link: "https://researchr.org/alias/gabriel-ebner"
  - name: "Sebastian Ullrich"
    link: "https://pp.ipd.kit.edu/~ullrich/?lang=en"
  - name: "Jared Roesch"
    link: "https://researchr.org/alias/jared-roesch"
  - name: "Jeremy Avigad"
    link: "https://researchr.org/alias/jeremy-avigad"
  - name: "Leonardo de Moura"
    link: "https://researchr.org/alias/leonardo-de-moura"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3110278"
  links:
    doi: "http://doi.acm.org/10.1145/3110278"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/EbnerURAM17"
  researchr: "https://researchr.org/publication/EbnerURAM17"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "1"
  number: "ICFP"
  kind: "article"
  key: "EbnerURAM17"
- title: "Universe Polymorphism in Coq"
  author:
  - name: "Matthieu Sozeau"
    link: "https://researchr.org/alias/matthieu-sozeau"
  - name: "Nicolas Tabareau"
    link: "https://researchr.org/alias/nicolas-tabareau"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-319-08970-6_32"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-08970-6_32"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/SozeauT14"
  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:
  - name: "Gerwin Klein"
    link: "https://researchr.org/alias/gerwin-klein"
  - name: "Ruben Gamboa"
    link: "https://researchr.org/alias/ruben-gamboa"
  volume: "8558"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-08969-0"
  kind: "inproceedings"
  key: "SozeauT14"
- title: "A tutorial implementation of dynamic pattern unification: A dependently typed programming language implementation pearl"
  author:
  - name: "Adam Gundry"
    link: "https://researchr.org/alias/adam-gundry"
  - name: "Conor McBride"
    link: "http://personal.cis.strath.ac.uk/~conor/"
  year: "2012"
  researchr: "https://researchr.org/publication/Gundry2012"
  cites: 0
  citedby: 0
  kind: "unpublished"
  key: "Gundry2012"
- title: "An Existential Crisis Resolved: Type inference for first-class existential types "
  author:
  - name: "Richard A. Eisenberg"
    link: "https://researchr.org/alias/richard-a.-eisenberg"
  - name: " Guillaume Duboc"
    link: "https://researchr.org/alias/guillaume-duboc"
  - name: "Stephanie Weirich"
    link: "https://researchr.org/alias/stephanie-weirich"
  - name: "Daniel Lee"
    link: "https://researchr.org/alias/daniel-lee"
  year: "2021"
  researchr: "https://researchr.org/publication/Eisenberg2021"
  cites: 0
  citedby: 0
  kind: "unpublished"
  key: "Eisenberg2021"
- title: "An algorithm for testing conversion in type theory"
  author:
  - name: "Coquand, Thierry"
    link: "https://researchr.org/alias/coquand%2C-thierry"
  year: "1991"
  researchr: "https://researchr.org/publication/coquand1991algorithm"
  cites: 0
  citedby: 0
  journal: "Logical frameworks"
  volume: "1"
  pages: "255-279"
  kind: "article"
  key: "coquand1991algorithm"
- title: "A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions"
  author:
  - name: "Andrea Asperti"
    link: "https://researchr.org/alias/andrea-asperti"
  - name: "Wilmer Ricciotti"
    link: "https://researchr.org/alias/wilmer-ricciotti"
  - name: "Claudio Sacerdoti Coen"
    link: "https://researchr.org/alias/claudio-sacerdoti-coen"
  - name: "Enrico Tassi"
    link: "https://researchr.org/alias/enrico-tassi"
  year: "2012"
  doi: "10.2168/LMCS-8(1:18)2012"
  links:
    "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"
  kind: "article"
  key: "DBLP:journals-corr-abs-1202-4905"
- title: "A quick look at impredicativity"
  author:
  - name: "Alejandro Serrano 0001"
    link: "https://researchr.org/alias/alejandro-serrano-0001"
  - name: "Jurriaan Hage"
    link: "https://researchr.org/alias/jurriaan-hage"
  - name: "Simon Peyton Jones"
    link: "https://researchr.org/alias/simon-peyton-jones"
  - name: "Dimitrios Vytiniotis"
    link: "https://researchr.org/alias/dimitrios-vytiniotis"
  year: "2020"
  doi: "https://doi.org/10.1145/3408971"
  links:
    doi: "https://doi.org/10.1145/3408971"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/SerranoHJV20"
  researchr: "https://researchr.org/publication/SerranoHJV20"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "4"
  number: "ICFP"
  kind: "article"
  key: "SerranoHJV20"
- title: "An insider's look at LF type reconstruction: everything you (n)ever wanted to know"
  author:
  - name: "Brigitte Pientka"
    link: "https://researchr.org/alias/brigitte-pientka"
  year: "2013"
  doi: "http://dx.doi.org/10.1017/S0956796812000408"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796812000408"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/Pientka13"
  researchr: "https://researchr.org/publication/Pientka13"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "23"
  number: "1"
  pages: "1-37"
  kind: "article"
  key: "Pientka13"
- title: "Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions"
  author:
  - name: "Kathrin Stark"
    link: "https://researchr.org/alias/kathrin-stark"
  - name: "Steven Schäfer"
    link: "https://researchr.org/alias/steven-sch%C3%A4fer"
  - name: "Jonas Kaiser"
    link: "https://researchr.org/alias/jonas-kaiser"
  year: "2019"
  doi: "https://doi.org/10.1145/3293880.3294101"
  links:
    doi: "https://doi.org/10.1145/3293880.3294101"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/StarkSK19"
  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:
  - name: "Assia Mahboubi"
    link: "https://researchr.org/alias/assia-mahboubi"
  - name: "Magnus O. Myreen"
    link: "https://researchr.org/alias/magnus-o.-myreen"
  publisher: "ACM"
  isbn: "978-1-4503-6222-1"
  kind: "inproceedings"
  key: "StarkSK19"
- title: "Elaborating dependent (co)pattern matching: No pattern left behind"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  year: "2020"
  doi: "https://doi.org/10.1017/S0956796819000182"
  links:
    doi: "https://doi.org/10.1017/S0956796819000182"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/CockxA20"
  researchr: "https://researchr.org/publication/CockxA20"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "30"
  kind: "article"
  key: "CockxA20"
- title: "GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and laziness"
  author:
  - name: "Georgios Karachalias"
    link: "https://researchr.org/alias/georgios-karachalias"
  - name: "Tom Schrijvers"
    link: "https://researchr.org/alias/tom-schrijvers"
  - name: "Dimitrios Vytiniotis"
    link: "https://researchr.org/alias/dimitrios-vytiniotis"
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  year: "2015"
  doi: "http://doi.acm.org/10.1145/2784731.2784748"
  links:
    doi: "http://doi.acm.org/10.1145/2784731.2784748"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/KarachaliasSVJ15"
  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:
  - name: "Kathleen Fisher"
    link: "https://researchr.org/alias/kathleen-fisher"
  - name: "John H. Reppy"
    link: "https://researchr.org/alias/john-h.-reppy"
  publisher: "ACM"
  isbn: "978-1-4503-3669-7"
  kind: "inproceedings"
  key: "KarachaliasSVJ15"
- title: "Tabled Typeclass Resolution"
  author:
  - name: "Daniel Selsam"
    link: "https://researchr.org/alias/daniel-selsam"
  - name: "Sebastian Ullrich"
    link: "https://pp.ipd.kit.edu/~ullrich/?lang=en"
  - name: "Leonardo de Moura"
    link: "https://researchr.org/alias/leonardo-de-moura"
  year: "2020"
  links:
    "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"
  kind: "article"
  key: "DBLP:journals-corr-abs-2001-04301"
- title: "A New Implementation of Automath"
  author:
  - name: "Freek Wiedijk"
    link: "http://www.cs.ru.nl/~freek/"
  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"
  kind: "article"
  key: "Wiedijk02"
- title: "Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions"
  author:
  - name: "Steven Schäfer"
    link: "https://researchr.org/alias/steven-sch%C3%A4fer"
  - name: "Tobias Tebbi"
    link: "https://researchr.org/alias/tobias-tebbi"
  - name: "Gert Smolka"
    link: "https://researchr.org/alias/gert-smolka"
  year: "2015"
  doi: "http://dx.doi.org/10.1007/978-3-319-22102-1_24"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-22102-1_24"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/SchaferTS15"
  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:
  - name: "Christian Urban"
    link: "https://researchr.org/alias/christian-urban"
  - name: "Xingyuan Zhang"
    link: "https://researchr.org/alias/xingyuan-zhang"
  volume: "9236"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-22101-4"
  kind: "inproceedings"
  key: "SchaferTS15"
- title: "Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications"
  author:
  - name: "Arjen Rouvoet"
    link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/"
  - name: "Hendrik van Antwerpen"
    link: "https://researchr.org/alias/hendrik-van-antwerpen"
  - name: "Casper Bach Poulsen"
    link: "http://www.casperbp.net"
  - name: "Robbert Krebbers"
    link: "https://researchr.org/alias/robbert-krebbers"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2020"
  doi: "https://doi.org/10.1145/3428248"
  abstract: "There is a large gap between the specification of type systems and the implementation of their type checkers, which impedes reasoning about the soundness of the type checker with respect to the specification. A vision to close this gap is to automatically obtain type checkers from declarative programming language specifications. This moves the burden of proving correctness from a case-by-case basis for concrete languages to a single correctness proof for the specification language. This vision is obstructed by an aspect common to all programming languages: name resolution. Naming and scoping are pervasive and complex aspects of the static semantics of programming languages. Implementations of type checkers for languages with name binding features such as modules, imports, classes, and inheritance interleave collection of binding information (i.e., declarations, scoping structure, and imports) and querying that information. This requires scheduling those two aspects in such a way that query answers are stable—i.e., they are computed only after all relevant binding structure has been collected. Type checkers for concrete languages accomplish stability using language-specific knowledge about the type system. In this paper we give a language-independent characterization of necessary and sufficient conditions to guarantee stability of name and type queries during type checking in terms of critical edges in an incomplete scope graph. We use critical edges to give a formal small-step operational semantics to a declarative specification language for type systems, that achieves soundness by delaying queries that may depend on missing information. This yields type checkers for the specified languages that are sound by construction—i.e., they schedule queries so that the answers are stable, and only accept programs that are name- and type-correct according to the declarative language specification. We implement this approach, and evaluate it against specifications of a small module and record language, as well as subsets of Java and Scala."
  links:
    doi: "https://doi.org/10.1145/3428248"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/RouvoetAPKV20"
  researchr: "https://researchr.org/publication/RouvoetAPKV20"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "4"
  number: "OOPSLA"
  kind: "article"
  key: "RouvoetAPKV20"
- title: "Practical dependent type checking using twin types"
  author:
  - name: "Víctor López Juan"
    link: "https://researchr.org/alias/v%C3%ADctor-l%C3%B3pez-juan"
  - name: "Nils Anders Danielsson"
    link: "https://researchr.org/alias/nils-anders-danielsson"
  year: "2020"
  doi: "https://doi.org/10.1145/3406089.3409030"
  links:
    doi: "https://doi.org/10.1145/3406089.3409030"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/JuanD20"
  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:
  - name: "James McKinna"
    link: "https://researchr.org/alias/james-mckinna"
  - name: "Cyrus Omar"
    link: "https://researchr.org/alias/cyrus-omar"
  publisher: "ACM"
  isbn: "978-1-4503-8051-5"
  kind: "inproceedings"
  key: "JuanD20"
- title: "Dependent type systems as macros"
  author:
  - name: "Stephen Chang"
    link: "https://researchr.org/alias/stephen-chang"
  - name: "Michael Ballantyne"
    link: "https://researchr.org/alias/michael-ballantyne"
  - name: "Milo Turner"
    link: "https://researchr.org/alias/milo-turner"
  - name: "William J. Bowman"
    link: "https://researchr.org/alias/william-j.-bowman"
  year: "2020"
  doi: "https://doi.org/10.1145/3371071"
  links:
    doi: "https://doi.org/10.1145/3371071"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/ChangBTB20"
  researchr: "https://researchr.org/publication/ChangBTB20"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "4"
  number: "POPL"
  kind: "article"
  key: "ChangBTB20"