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: "cade"
  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: "PACMPL"
  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: "TYPES"
  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: "JFP"
  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: "ICFP"
  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: "lics"
  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: "fscd"
  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: "PACMPL"
  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: "PACMPL"
  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: "TYPES"
  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: "cade"
  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: "tphol"
  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: "PACMPL"
  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: "ICFP"
  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: "cade"
  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: "IFL"
  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: "lpar"
  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: "cade"
  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"
  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: "ICLP"
  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: "sdt"
  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: "tlca"
  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: "JAR"
  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"
  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: "cade"
  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"
  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: "TOPLAS"
  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"
  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: "RTA"
  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: "itp"
  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: "ESOP"
  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: "sfp"
  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"
  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: "haskell"
  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: "PACMPL"
  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: "SCP"
  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: "mscs"
  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: "PACMPL"
  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"
  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: "ENTCS"
  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: "tphol"
  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: "TOPLAS"
  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: "cade"
  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: "POPL"
  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: "ppdp"
  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"
  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: "FUIN"
  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: "JFP"
  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"
  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: "JFP"
  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"
  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: "JFP"
  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: "PACMPL"
  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: "itp"
  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: "PACMPL"
  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: "JFP"
  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: "CPP"
  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: "JFP"
  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: "ICFP"
  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: "JAR"
  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: "itp"
  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: "PACMPL"
  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: "ICFP"
  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: "PACMPL"
  volume: "4"
  number: "POPL"
  kind: "article"
  key: "ChangBTB20"