publications:
- title: "Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type"
  author:
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  - name: "Nils Anders Danielsson"
    link: "https://researchr.org/alias/nils-anders-danielsson"
  - name: "Nicolai Kraus"
    link: "https://researchr.org/alias/nicolai-kraus"
  year: "2017"
  doi: "http://dx.doi.org/10.1007/978-3-662-54458-7_31"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-662-54458-7_31"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fossacs/AltenkirchDK17"
  researchr: "https://researchr.org/publication/AltenkirchDK17"
  cites: 0
  citedby: 0
  pages: "534-549"
  booktitle: "fossacs"
  kind: "inproceedings"
  key: "AltenkirchDK17"
- title: "Representing Agda and coinduction in the $\\lambda$$\\Pi$-calculus modulo rewriting"
  author:
  - name: "Felicissimo, Thiago"
    link: "https://researchr.org/alias/felicissimo%2C-thiago"
  year: "2021"
  month: "Sep"
  links:
    "url": "https://hal.inria.fr/hal-03343699"
  researchr: "https://researchr.org/publication/felicissimo%3Ahal-03343699"
  cites: 0
  citedby: 0
  school: "LSV, ENS Paris Saclay, Universit{\\'e} Paris-Saclay"
  kind: "mastersthesis"
  key: "felicissimo:hal-03343699"
- title: "A Mechanised Abstract Formalisation of Concept Lattices"
  author:
  - name: "Wolfram Kahl"
    link: "https://researchr.org/alias/wolfram-kahl"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-319-06251-8_15"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-06251-8_15"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/RelMiCS/Kahl14"
  researchr: "https://researchr.org/publication/Kahl14"
  cites: 0
  citedby: 0
  pages: "242-260"
  booktitle: "RelMiCS"
  kind: "inproceedings"
  key: "Kahl14"
- title: "Towards a formal semantics for a structurally dynamic noncausal modelling language"
  author:
  - name: "John Capper"
    link: "https://researchr.org/alias/john-capper"
  - name: "Henrik Nilsson"
    link: "https://researchr.org/alias/henrik-nilsson"
  year: "2012"
  doi: "http://doi.acm.org/10.1145/2103786.2103792"
  links:
    doi: "http://doi.acm.org/10.1145/2103786.2103792"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tldi/CapperN12"
  researchr: "https://researchr.org/publication/CapperN12"
  cites: 0
  citedby: 0
  pages: "39-50"
  booktitle: "tldi"
  kind: "inproceedings"
  key: "CapperN12"
- title: "Constructing quotient inductive-inductive types"
  author:
  - name: "Ambrus Kaposi"
    link: "https://researchr.org/alias/ambrus-kaposi"
  - name: "András Kovács"
    link: "https://researchr.org/alias/andr%C3%A1s-kov%C3%A1cs"
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  year: "2019"
  doi: "https://dl.acm.org/citation.cfm?id=3290315"
  links:
    doi: "https://dl.acm.org/citation.cfm?id=3290315"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/KaposiKA19"
  researchr: "https://researchr.org/publication/KaposiKA19"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "3"
  kind: "article"
  key: "KaposiKA19"
- title: "Generalized Universe Hierarchies and First-Class Universe Levels"
  author:
  - name: "András Kovács"
    link: "https://researchr.org/alias/andr%C3%A1s-kov%C3%A1cs"
  year: "2022"
  doi: "https://doi.org/10.4230/LIPIcs.CSL.2022.28"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.CSL.2022.28"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/Kovacs22"
  researchr: "https://researchr.org/publication/Kovacs22"
  cites: 0
  citedby: 0
  booktitle: "csl"
  kind: "inproceedings"
  key: "Kovacs22"
- title: "The Lax Braided Structure of Streaming I/O"
  author:
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  - name: "Julian Rathke"
    link: "https://researchr.org/alias/julian-rathke"
  year: "2011"
  doi: "http://dx.doi.org/10.4230/LIPIcs.CSL.2011.292"
  links:
    doi: "http://dx.doi.org/10.4230/LIPIcs.CSL.2011.292"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/JeffreyR11"
  researchr: "https://researchr.org/publication/JeffreyR11"
  cites: 0
  citedby: 0
  pages: "292-306"
  booktitle: "csl"
  kind: "inproceedings"
  key: "JeffreyR11"
- title: "Intrinsically-typed definitional interpreters for linear, session-typed languages"
  author:
  - name: "Arjen Rouvoet"
    link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/"
  - name: "Casper Bach Poulsen"
    link: "http://www.casperbp.net"
  - name: "Robbert Krebbers"
    link: "https://robbertkrebbers.nl"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2020"
  doi: "https://doi.org/10.1145/3372885.3373818"
  abstract: "An intrinsically-typed definitional interpreter is a concise specification of dynamic semantics, that is executable and type safe by construction. Unfortunately, scaling intrinsically-typed definitional interpreters to more complicated object languages often results in definitions that are cluttered with manual proof work. For linearly-typed languages (including session-typed languages) one has to prove that the interpreter, as well as all the operations on semantic components, treat values linearly. We present new methods and tools that make it possible to implement intrinsically-typed definitional interpreters for linearly-typed languages in a way that hides the majority of the manual proof work. Inspired by separation logic, we develop reusable and composable abstractions for programming with linear operations using dependent types. Using these abstractions, we define interpreters for linear lambda calculi with strong references, concurrency, and session-typed communication in Agda."
  links:
    doi: "https://doi.org/10.1145/3372885.3373818"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/RouvoetPKV20"
  researchr: "https://researchr.org/publication/RouvoetPKV20"
  cites: 0
  citedby: 0
  pages: "284-298"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "RouvoetPKV20"
- title: "Focusing on Binding and Computation"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Noam Zeilberger"
    link: "https://researchr.org/alias/noam-zeilberger"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2008"
  doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2008.48"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2008.48"
  researchr: "https://researchr.org/publication/LicataZH08"
  cites: 0
  citedby: 0
  pages: "241-252"
  booktitle: "lics"
  kind: "inproceedings"
  key: "LicataZH08"
- title: "A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory"
  author:
  - name: "Kuen-Bang Hou (Favonia)"
    link: "https://researchr.org/alias/kuen-bang-hou-%28favonia%29"
  - name: "Eric Finster"
    link: "https://researchr.org/alias/eric-finster"
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Peter LeFanu Lumsdaine"
    link: "https://researchr.org/alias/peter-lefanu-lumsdaine"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2933575.2934545"
  links:
    doi: "http://doi.acm.org/10.1145/2933575.2934545"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/FavoniaFLL16"
  researchr: "https://researchr.org/publication/FavoniaFLL16"
  cites: 0
  citedby: 0
  pages: "565-574"
  booktitle: "lics"
  kind: "inproceedings"
  key: "FavoniaFLL16"
- title: "Embedding a logical theory of constructions in Agda"
  author:
  - name: "Ana Bove"
    link: "https://researchr.org/alias/ana-bove"
  - name: "Peter Dybjer"
    link: "https://researchr.org/alias/peter-dybjer"
  - name: "Andrés Sicard-Ramírez"
    link: "https://researchr.org/alias/andr%C3%A3%C2%A9s-sicard-ram%C3%A3%C2%ADrez"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1481848.1481857"
  links:
    doi: "http://doi.acm.org/10.1145/1481848.1481857"
  researchr: "https://researchr.org/publication/BoveDS09"
  cites: 0
  citedby: 0
  pages: "59-66"
  booktitle: "plpv"
  kind: "inproceedings"
  key: "BoveDS09"
- title: "Indexed Containers"
  author:
  - name: "Thorsten Altenkirch"
    link: "http://www.cs.nott.ac.uk/~txa"
  - name: "Peter Morris"
    link: "https://researchr.org/alias/peter-morris"
  year: "2009"
  doi: "http://dx.doi.org/10.1109/LICS.2009.33"
  links:
    doi: "http://dx.doi.org/10.1109/LICS.2009.33"
  researchr: "https://researchr.org/publication/AltenkirchM09"
  cites: 0
  citedby: 0
  pages: "277-285"
  booktitle: "lics"
  kind: "inproceedings"
  key: "AltenkirchM09"
- title: "The Seifert-van Kampen Theorem in Homotopy Type Theory"
  author:
  - name: "Kuen-Bang Hou (Favonia)"
    link: "https://researchr.org/alias/kuen-bang-hou-%28favonia%29"
  - name: "Michael Shulman"
    link: "https://researchr.org/alias/michael-shulman"
  year: "2016"
  doi: "http://dx.doi.org/10.4230/LIPIcs.CSL.2016.22"
  links:
    doi: "http://dx.doi.org/10.4230/LIPIcs.CSL.2016.22"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/FavoniaS16"
  researchr: "https://researchr.org/publication/FavoniaS16"
  cites: 0
  citedby: 0
  booktitle: "csl"
  kind: "inproceedings"
  key: "FavoniaS16"
- title: "Automating Boundary Filling in Cubical Agda"
  author:
  - name: "Maximilian Doré"
    link: "https://researchr.org/alias/maximilian-dor%C3%A9"
  - name: "Evan Cavallo"
    link: "https://researchr.org/alias/evan-cavallo"
  - name: "Anders Mörtberg"
    link: "https://researchr.org/alias/anders-m%C3%B6rtberg"
  year: "2024"
  doi: "https://doi.org/10.4230/LIPIcs.FSCD.2024.22"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.FSCD.2024.22"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fscd/DoreCM24"
  researchr: "https://researchr.org/publication/DoreCM24"
  cites: 0
  citedby: 0
  booktitle: "fscd"
  kind: "inproceedings"
  key: "DoreCM24"
- title: "Generic packet descriptions: verified parsing and pretty printing of low-level data"
  author:
  - name: "Marcell van Geest"
    link: "https://researchr.org/alias/marcell-van-geest"
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  year: "2017"
  doi: "https://doi.org/10.1145/3122975.3122979"
  links:
    doi: "https://doi.org/10.1145/3122975.3122979"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/GeestS17"
  researchr: "https://researchr.org/publication/GeestS17"
  cites: 0
  citedby: 0
  pages: "30-40"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "GeestS17"
- title: "Indexed containers"
  author:
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  - name: "Neil Ghani"
    link: "https://researchr.org/alias/neil-ghani"
  - name: "Peter Hancock"
    link: "https://researchr.org/alias/peter-hancock"
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  - name: "Peter Morris"
    link: "https://researchr.org/alias/peter-morris"
  year: "2015"
  doi: "http://dx.doi.org/10.1017/S095679681500009X"
  links:
    doi: "http://dx.doi.org/10.1017/S095679681500009X"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/AltenkirchGHMM15"
  researchr: "https://researchr.org/publication/AltenkirchGHMM15"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "25"
  kind: "article"
  key: "AltenkirchGHMM15"
- title: "A continuous computational interpretation of type theories"
  author:
  - name: "Chuangjie Xu"
    link: "https://researchr.org/alias/chuangjie-xu"
  year: "2015"
  doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.649340"
  links:
    doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.649340"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/ethos/Xu15a"
  researchr: "https://researchr.org/publication/ethos-10314"
  cites: 0
  citedby: 0
  school: "University of Birmingham, UK"
  kind: "phdthesis"
  key: "ethos-10314"
- title: "Deeper Shallow Embeddings"
  author:
  - name: "Jacob Prinz"
    link: "https://researchr.org/alias/jacob-prinz"
  - name: "G. A. Kavvos"
    link: "https://researchr.org/alias/g.-a.-kavvos"
  - name: "Leonidas Lampropoulos"
    link: "https://researchr.org/alias/leonidas-lampropoulos"
  year: "2022"
  doi: "https://doi.org/10.4230/LIPIcs.ITP.2022.28"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.ITP.2022.28"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/PrinzKL22"
  researchr: "https://researchr.org/publication/PrinzKL22"
  cites: 0
  citedby: 0
  booktitle: "itp"
  kind: "inproceedings"
  key: "PrinzKL22"
- title: "The Sequent Calculus of Skew Monoidal Categories"
  author:
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  - name: "Noam Zeilberger"
    link: "https://researchr.org/alias/noam-zeilberger"
  year: "2018"
  doi: "https://doi.org/10.1016/j.entcs.2018.11.017"
  links:
    doi: "https://doi.org/10.1016/j.entcs.2018.11.017"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/entcs/UustaluVZ18"
  researchr: "https://researchr.org/publication/UustaluVZ18"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "341"
  pages: "345-370"
  kind: "article"
  key: "UustaluVZ18"
- title: "Arity-generic datatype-generic programming"
  author:
  - name: "Stephanie Weirich"
    link: "https://researchr.org/alias/stephanie-weirich"
  - name: "Chris Casinghino"
    link: "https://researchr.org/alias/chris-casinghino"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1707790.1707799"
  abstract: "Some programs are doubly-generic. For example, map is datatype-generic in that many different data structures support a mapping operation. A generic programming language like Generic Haskell can use a single definition to generate map for each type. However, map is also arity-generic because it belongs to a family of related operations that differ in the number of arguments. For lists, this family includes repeat, map, zipWith, zipWith3, zipWith4, etc. With dependent types or clever programming, one can unify all of these functions together in a single definition. However, no one has explored the combination of these two forms of genericity. These two axes are not orthogonal because the idea of arity appears in Generic Haskell: datatype-generic versions of repeat, map and zipWith have different arities of kind-indexed types. In this paper, we define arity-generic datatype-generic programs by building a framework for Generic Haskell-style generic programming in the dependently-typed programming language Agda 2."
  links:
    doi: "http://doi.acm.org/10.1145/1707790.1707799"
  tags:
  - "programming languages"
  - "data-flow language"
  - "generic programming"
  - "Haskell"
  - "data-flow programming"
  - "data-flow"
  - "programming"
  researchr: "https://researchr.org/publication/WeirichC10"
  cites: 0
  citedby: 0
  pages: "15-26"
  booktitle: "plpv"
  kind: "inproceedings"
  key: "WeirichC10"
- title: "Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2018"
  doi: "https://doi.org/10.1017/S095679681800014X"
  links:
    doi: "https://doi.org/10.1017/S095679681800014X"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/CockxD18"
  researchr: "https://researchr.org/publication/CockxD18"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "28"
  kind: "article"
  key: "CockxD18"
- title: "Dependently Typed Programming in Agda"
  author:
  - name: "Ulf Norell"
    link: "http://www.cse.chalmers.se/~ulfn/"
  year: "2008"
  doi: "http://dx.doi.org/10.1007/978-3-642-04652-0_5"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-04652-0_5"
  tags:
  - "programming"
  researchr: "https://researchr.org/publication/Norell08"
  cites: 0
  citedby: 0
  pages: "230-266"
  booktitle: "afp"
  kind: "inproceedings"
  key: "Norell08"
- title: "The gentle art of levitation"
  author:
  - name: "James Chapman"
    link: "https://researchr.org/alias/james-chapman"
  - name: "Pierre-Évariste Dagand"
    link: "https://researchr.org/alias/pierre-%C3%A9variste-dagand"
  - name: "Conor McBride"
    link: "http://personal.cis.strath.ac.uk/~conor/"
  - name: "Peter Morris"
    link: "https://researchr.org/alias/peter-morris"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863543.1863547"
  links:
    doi: "http://doi.acm.org/10.1145/1863543.1863547"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/ChapmanDMM10"
  researchr: "https://researchr.org/publication/ChapmanDMM10"
  cites: 0
  citedby: 0
  pages: "3-14"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "ChapmanDMM10"
- title: "A completely unique account of enumeration"
  author:
  - name: "Cas van der Rest"
    link: "https://researchr.org/alias/cas-van-der-rest"
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  year: "2022"
  doi: "https://doi.org/10.1145/3547636"
  links:
    doi: "https://doi.org/10.1145/3547636"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/RestS22"
  researchr: "https://researchr.org/publication/RestS22"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "6"
  number: "ICFP"
  pages: "411-437"
  kind: "article"
  key: "RestS22"
- title: "A Dependently Typed Linear π-Calculus in Agda"
  author:
  - name: "Luca Ciccone"
    link: "https://researchr.org/alias/luca-ciccone"
  - name: "Luca Padovani"
    link: "https://researchr.org/alias/luca-padovani"
  year: "2020"
  doi: "https://doi.org/10.1145/3414080.3414109"
  links:
    doi: "https://doi.org/10.1145/3414080.3414109"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/CicconeP20"
  researchr: "https://researchr.org/publication/CicconeP20"
  cites: 0
  citedby: 0
  booktitle: "ppdp"
  kind: "inproceedings"
  key: "CicconeP20"
- title: "Axioms for Modelling Cubical Type Theory in a Topos"
  author:
  - name: "Ian Orton"
    link: "https://researchr.org/alias/ian-orton"
  - name: "Andrew M. Pitts"
    link: "https://researchr.org/alias/andrew-m.-pitts"
  year: "2016"
  doi: "http://dx.doi.org/10.4230/LIPIcs.CSL.2016.24"
  links:
    doi: "http://dx.doi.org/10.4230/LIPIcs.CSL.2016.24"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/OrtonP16"
  researchr: "https://researchr.org/publication/OrtonP16"
  cites: 0
  citedby: 0
  booktitle: "csl"
  kind: "inproceedings"
  key: "OrtonP16"
- title: "BiSikkel: A Multimode Logical Framework in Agda"
  author:
  - name: "Joris Ceulemans"
    link: "https://researchr.org/alias/joris-ceulemans"
  - name: "Andreas Nuyts"
    link: "https://researchr.org/alias/andreas-nuyts"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2025"
  doi: "https://doi.org/10.1145/3704844"
  links:
    doi: "https://doi.org/10.1145/3704844"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/CeulemansND25"
  researchr: "https://researchr.org/publication/CeulemansND25"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "9"
  number: "POPL"
  pages: "210-240"
  kind: "article"
  key: "CeulemansND25"
- title: "Dependent Types at Work"
  author:
  - name: "Ana Bove"
    link: "https://researchr.org/alias/ana-bove"
  - name: "Peter Dybjer"
    link: "https://researchr.org/alias/peter-dybjer"
  year: "2008"
  doi: "http://dx.doi.org/10.1007/978-3-642-03153-3_2"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-03153-3_2"
  researchr: "https://researchr.org/publication/BoveD08"
  cites: 0
  citedby: 0
  pages: "57-99"
  booktitle: "lernet"
  kind: "inproceedings"
  key: "BoveD08"
- title: "A theory of higher-order subtyping with type intervals"
  author:
  - name: "Sandro Stucki"
    link: "https://researchr.org/alias/sandro-stucki"
  - name: " Paolo G. Giarrusso"
    link: "https://researchr.org/alias/paolo-g.-giarrusso"
  year: "2021"
  doi: "https://doi.org/10.1145/3473574"
  links:
    doi: "https://doi.org/10.1145/3473574"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/StuckiG21"
  researchr: "https://researchr.org/publication/StuckiG21"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "5"
  number: "ICFP"
  pages: "1-30"
  kind: "article"
  key: "StuckiG21"
- title: "Formal verification of authenticated, append-only skip lists in Agda"
  author:
  - name: "Victor Cacciari Miraldo"
    link: "https://researchr.org/alias/victor-cacciari-miraldo"
  - name: "Harold Carr"
    link: "https://researchr.org/alias/harold-carr"
  - name: "Mark Moir"
    link: "https://researchr.org/alias/mark-moir"
  - name: "Lisandra Silva"
    link: "https://researchr.org/alias/lisandra-silva"
  - name: "Guy L. Steele Jr."
    link: "https://researchr.org/alias/guy-l.-steele-jr."
  year: "2021"
  doi: "https://doi.org/10.1145/3437992.3439924"
  links:
    doi: "https://doi.org/10.1145/3437992.3439924"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/MiraldoCMSS21"
  researchr: "https://researchr.org/publication/MiraldoCMSS21"
  cites: 0
  citedby: 0
  pages: "122-136"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "MiraldoCMSS21"
- title: "Compiling Concurrency Correctly: Cutting out the Middle Man"
  author:
  - name: "Liyang Hu"
    link: "https://researchr.org/alias/liyang-hu"
  - name: "Graham Hutton"
    link: "https://researchr.org/alias/graham-hutton"
  year: "2009"
  links:
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sfp/HuH09"
  researchr: "https://researchr.org/publication/HuH09-9"
  cites: 0
  citedby: 0
  pages: "17-32"
  booktitle: "sfp"
  kind: "inproceedings"
  key: "HuH09-9"
- title: "Auto in Agda - Programming Proof Search Using Reflection"
  author:
  - name: "Pepijn Kokke"
    link: "https://researchr.org/alias/pepijn-kokke"
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  year: "2015"
  doi: "http://dx.doi.org/10.1007/978-3-319-19797-5_14"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-19797-5_14"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/mpc/KokkeS15"
  researchr: "https://researchr.org/publication/KokkeS15"
  cites: 0
  citedby: 0
  pages: "276-301"
  booktitle: "mpc"
  kind: "inproceedings"
  key: "KokkeS15"
- title: "A Formalized Proof of Strong Normalization for Guarded Recursive Types"
  author:
  - name: "Andreas Abel"
    link: "https://researchr.org/alias/andreas-abel"
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-319-12736-1_8"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-12736-1_8"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/aplas/AbelV14"
  researchr: "https://researchr.org/publication/AbelV14"
  cites: 0
  citedby: 0
  pages: "140-158"
  booktitle: "aplas"
  kind: "inproceedings"
  key: "AbelV14"
- title: "Beating the Productivity Checker Using Embedded Languages"
  author:
  - name: "Nils Anders Danielsson"
    link: "https://researchr.org/alias/nils-anders-danielsson"
  year: "2010"
  doi: "http://www.easychair.org/publications/?page=350518201"
  links:
    doi: "http://www.easychair.org/publications/?page=350518201"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/Danielsson10"
  researchr: "https://researchr.org/publication/Danielsson10-1"
  cites: 0
  citedby: 0
  pages: "33-53"
  booktitle: "itp"
  kind: "inproceedings"
  key: "Danielsson10-1"
- title: "Homotopical patch theory"
  author:
  - name: "Carlo Angiuli"
    link: "https://researchr.org/alias/carlo-angiuli"
  - name: "Edward Morehouse"
    link: "https://researchr.org/alias/edward-morehouse"
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2016"
  doi: "http://dx.doi.org/10.1017/S0956796816000198"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796816000198"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/AngiuliMLH16"
  researchr: "https://researchr.org/publication/AngiuliMLH16"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "26"
  kind: "article"
  key: "AngiuliMLH16"
- title: "Dependently Typed Web Client Applications - FRP in Agda in HTML5"
  author:
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2013"
  doi: "http://dx.doi.org/10.1007/978-3-642-45284-0_16"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-45284-0_16"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/padl/Jeffrey13"
  researchr: "https://researchr.org/publication/Jeffrey13-1"
  cites: 0
  citedby: 0
  pages: "228-243"
  booktitle: "PADL"
  kind: "inproceedings"
  key: "Jeffrey13-1"
- title: "Formalizing category theory in Agda"
  author:
  - name: "Jason Z. S. Hu"
    link: "https://researchr.org/alias/jason-z.-s.-hu"
  - name: "Jacques Carette"
    link: "https://researchr.org/alias/jacques-carette"
  year: "2021"
  doi: "https://doi.org/10.1145/3437992.3439922"
  links:
    doi: "https://doi.org/10.1145/3437992.3439922"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/HuC21"
  researchr: "https://researchr.org/publication/HuC21"
  cites: 0
  citedby: 0
  pages: "327-342"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "HuC21"
- title: "Positively dependent types"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1481848.1481851"
  links:
    doi: "http://doi.acm.org/10.1145/1481848.1481851"
  researchr: "https://researchr.org/publication/LicataH09-0"
  cites: 0
  citedby: 0
  pages: "3-14"
  booktitle: "plpv"
  kind: "inproceedings"
  key: "LicataH09-0"
- title: "Dependently-Typed Programming in Scientific Computing - Examples from Economic Modelling"
  author:
  - name: "Cezar Ionescu"
    link: "https://researchr.org/alias/cezar-ionescu"
  - name: "Patrik Jansson"
    link: "https://researchr.org/alias/patrik-jansson"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/978-3-642-41582-1_9"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-41582-1_9"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ifl/IonescuJ12"
  researchr: "https://researchr.org/publication/IonescuJ12"
  cites: 0
  citedby: 0
  pages: "140-156"
  booktitle: "IFL"
  kind: "inproceedings"
  key: "IonescuJ12"
- title: "On the bright side of type classes: instance arguments in Agda"
  author:
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/2034773.2034796"
  links:
    doi: "http://doi.acm.org/10.1145/2034773.2034796"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/DevrieseP11"
  researchr: "https://researchr.org/publication/DevrieseP11-1"
  cites: 0
  citedby: 0
  pages: "143-155"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "DevrieseP11-1"
- title: "Type Theory Should Eat Itself"
  author:
  - name: "James Chapman"
    link: "https://researchr.org/alias/james-chapman"
  year: "2009"
  doi: "http://dx.doi.org/10.1016/j.entcs.2008.12.114"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2008.12.114"
  tags:
  - "type theory"
  researchr: "https://researchr.org/publication/Chapman09"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "228"
  pages: "21-36"
  kind: "article"
  key: "Chapman09"
- title: "Focusing and higher-order abstract syntax"
  author:
  - name: "Noam Zeilberger"
    link: "https://researchr.org/alias/noam-zeilberger"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1328438.1328482"
  links:
    doi: "http://doi.acm.org/10.1145/1328438.1328482"
  tags:
  - "abstract syntax"
  researchr: "https://researchr.org/publication/Zeilberger08"
  cites: 0
  citedby: 0
  pages: "359-369"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "Zeilberger08"
- title: "Proofs for free - Parametricity for dependent types"
  author:
  - name: "Jean-Philippe Bernardy"
    link: "https://researchr.org/alias/jean-philippe-bernardy"
  - name: "Patrik Jansson"
    link: "https://researchr.org/alias/patrik-jansson"
  - name: "Ross Paterson"
    link: "https://researchr.org/alias/ross-paterson"
  year: "2012"
  doi: "http://dx.doi.org/10.1017/S0956796812000056"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796812000056"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/BernardyJP12"
  researchr: "https://researchr.org/publication/BernardyJP12"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "22"
  number: "2"
  pages: "107-152"
  kind: "article"
  key: "BernardyJP12"
- title: "Fibred Data Types"
  author:
  - name: "Neil Ghani"
    link: "https://researchr.org/alias/neil-ghani"
  - name: "Lorenzo Malatesta"
    link: "https://researchr.org/alias/lorenzo-malatesta"
  - name: "Fredrik Nordvall Forsberg"
    link: "https://researchr.org/alias/fredrik-nordvall-forsberg"
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  year: "2013"
  doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2013.30"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2013.30"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/GhaniMFS13"
  researchr: "https://researchr.org/publication/GhaniMFS13"
  cites: 0
  citedby: 0
  pages: "243-252"
  booktitle: "lics"
  kind: "inproceedings"
  key: "GhaniMFS13"
- title: "A Brief Overview of Agda - A Functional Language with Dependent Types"
  author:
  - name: "Ana Bove"
    link: "https://researchr.org/alias/ana-bove"
  - name: "Peter Dybjer"
    link: "https://researchr.org/alias/peter-dybjer"
  - name: "Ulf Norell"
    link: "http://www.cse.chalmers.se/~ulfn/"
  year: "2009"
  doi: "http://dx.doi.org/10.1007/978-3-642-03359-9_6"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-03359-9_6"
  researchr: "https://researchr.org/publication/BoveDN09"
  cites: 0
  citedby: 0
  pages: "73-78"
  booktitle: "tphol"
  kind: "inproceedings"
  key: "BoveDN09"
- 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: "The intrinsic topology of Martin-Löf universes"
  author:
  - name: "Martín Hötzel Escardó"
    link: "https://researchr.org/alias/mart%C3%ADn-h%C3%B6tzel-escard%C3%B3"
  - name: "Thomas Streicher"
    link: "https://researchr.org/alias/thomas-streicher"
  year: "2016"
  doi: "http://dx.doi.org/10.1016/j.apal.2016.04.010"
  links:
    doi: "http://dx.doi.org/10.1016/j.apal.2016.04.010"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/apal/EscardoS16"
  researchr: "https://researchr.org/publication/EscardoS16"
  cites: 0
  citedby: 0
  journal: "APAL"
  volume: "167"
  number: "9"
  pages: "794-805"
  kind: "article"
  key: "EscardoS16"
- title: "Type theory in type theory using quotient inductive types"
  author:
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  - name: "Ambrus Kaposi"
    link: "https://researchr.org/alias/ambrus-kaposi"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2837614.2837638"
  links:
    doi: "http://doi.acm.org/10.1145/2837614.2837638"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/AltenkirchK16"
  researchr: "https://researchr.org/publication/AltenkirchK16"
  cites: 0
  citedby: 0
  pages: "18-29"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "AltenkirchK16"
- title: "The Agda Universal Algebra Library, Part 1: Foundation"
  author:
  - name: "DeMeo, William"
    link: "https://researchr.org/alias/demeo%2C-william"
  year: "2021"
  doi: "10.48550/ARXIV.2103.05581"
  links:
    "url": "https://arxiv.org/abs/2103.05581"
  researchr: "https://researchr.org/publication/https%3A-doi.org-10.48550-arxiv.2103.05581"
  cites: 0
  citedby: 0
  kind: "misc"
  key: "https:-doi.org-10.48550-arxiv.2103.05581"
- title: "Monads Need Not Be Endofunctors"
  author:
  - name: "Thorsten Altenkirch"
    link: "http://www.cs.nott.ac.uk/~txa"
  - name: "James Chapman"
    link: "https://researchr.org/alias/james-chapman"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/978-3-642-12032-9_21"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-12032-9_21"
  researchr: "https://researchr.org/publication/AltenkirchCU10"
  cites: 0
  citedby: 0
  pages: "297-311"
  booktitle: "fossacs"
  kind: "inproceedings"
  key: "AltenkirchCU10"
- title: "Generic programming of all kinds"
  author:
  - name: "Alejandro Serrano"
    link: "https://researchr.org/alias/alejandro-serrano"
  - name: "Victor Cacciari Miraldo"
    link: "https://researchr.org/alias/victor-cacciari-miraldo"
  year: "2018"
  doi: "https://doi.org/10.1145/3242744.3242745"
  links:
    doi: "https://doi.org/10.1145/3242744.3242745"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/haskell/SerranoM18"
  researchr: "https://researchr.org/publication/SerranoM18"
  cites: 0
  citedby: 0
  pages: "41-54"
  booktitle: "haskell"
  kind: "inproceedings"
  key: "SerranoM18"
- title: "When Is a Type Refinement an Inductive Type?"
  author:
  - name: "Robert Atkey"
    link: "https://researchr.org/alias/robert-atkey"
  - name: "Patricia Johann"
    link: "https://researchr.org/alias/patricia-johann"
  - name: "Neil Ghani"
    link: "https://researchr.org/alias/neil-ghani"
  year: "2011"
  doi: "http://dx.doi.org/10.1007/978-3-642-19805-2_6"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-19805-2_6"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fossacs/AtkeyJG11"
  tags:
  - "refinement"
  researchr: "https://researchr.org/publication/AtkeyJG11"
  cites: 0
  citedby: 0
  pages: "72-87"
  booktitle: "fossacs"
  kind: "inproceedings"
  key: "AtkeyJG11"
- title: "Type-and-scope safe programs and their proofs"
  author:
  - name: "Guillaume Allais"
    link: "https://researchr.org/alias/guillaume-allais"
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  - name: "James McKinna"
    link: "https://researchr.org/alias/james-mckinna"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3018610.3018613"
  links:
    doi: "http://doi.acm.org/10.1145/3018610.3018613"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/Allais0MM17"
  tags:
  - "Intrinsic-Verification"
  researchr: "https://researchr.org/publication/Allais0MM17"
  cites: 0
  citedby: 0
  pages: "195-207"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "Allais0MM17"
- title: "A fresh look at programming with names and binders"
  author:
  - name: "Nicolas Pouillard"
    link: "https://researchr.org/alias/nicolas-pouillard"
  - name: "François Pottier"
    link: "https://researchr.org/alias/fran%C3%A7ois-pottier"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863543.1863575"
  links:
    doi: "http://doi.acm.org/10.1145/1863543.1863575"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/PouillardP10"
  tags:
  - "programming"
  researchr: "https://researchr.org/publication/PouillardP10"
  cites: 0
  citedby: 0
  pages: "217-228"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "PouillardP10"
- title: "Formalisation of Dependent Type Theory: The Example of CaTT"
  author:
  - name: "Thibaut Benjamin"
    link: "https://researchr.org/alias/thibaut-benjamin"
  year: "2021"
  doi: "https://doi.org/10.4230/LIPIcs.TYPES.2021.2"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.TYPES.2021.2"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/types/Benjamin21"
  researchr: "https://researchr.org/publication/Benjamin21-0"
  cites: 0
  citedby: 0
  booktitle: "TYPES"
  kind: "inproceedings"
  key: "Benjamin21-0"
- title: "Algebra of programming in Agda: Dependent types for relational program derivation"
  author:
  - name: "Shin-Cheng Mu"
    link: "http://www.iis.sinica.edu.tw/~scm/"
  - name: "Hsiang-Shang Ko"
    link: "http://joshkos.blogspot.se/"
  - name: "Patrik Jansson"
    link: "http://www.chalmers.se/cse/EN/people/jansson-patrik"
  year: "2009"
  doi: "http://dx.doi.org/10.1017/S0956796809007345"
  abstract: "Relational program derivation is the technique of stepwise refining a relational specification to a program by algebraic rules. The program thus obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express various correctness properties to be verified by the type checker. We have developed a library, AoPA (Algebra of Programming in Agda), to encode relational derivations in the dependently typed programming language Agda. A program is coupled with an algebraic derivation whose correctness is guaranteed by the type system. Two non-trivial examples are presented: an optimisation problem and a derivation of quicksort in which well-founded recursion is used to model terminating hylomorphisms in a language with inductive types."
  links:
    doi: "http://dx.doi.org/10.1017/S0956796809007345"
  tags:
  - "programming languages"
  - "rule-based"
  - "meta programming"
  - "program verification"
  - "meta-model"
  - "modeling language"
  - "language modeling"
  - "relational algebra"
  - "type system"
  - "rules"
  - "algebraic specification"
  - " algebra"
  - "programming"
  - "type theory"
  - "Meta-Environment"
  researchr: "https://researchr.org/publication/MuKJ09"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "19"
  number: "5"
  pages: "545-579"
  kind: "article"
  key: "MuKJ09"
- title: "The essence of ornaments"
  author:
  - name: "Pierre-Évariste Dagand"
    link: "https://researchr.org/alias/pierre-%C3%A9variste-dagand"
  year: "2017"
  doi: "http://dx.doi.org/10.1017/S0956796816000356"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796816000356"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/Dagand17"
  researchr: "https://researchr.org/publication/Dagand17"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "27"
  kind: "article"
  key: "Dagand17"
- title: "First-order natural deduction in Agda"
  author:
  - name: "Warren, Louis"
    link: "https://researchr.org/alias/warren%2C-louis"
  year: "2021"
  doi: "10.48550/ARXIV.2104.04095"
  links:
    "url": "https://arxiv.org/abs/2104.04095"
  researchr: "https://researchr.org/publication/https%3A-doi.org-10.48550-arxiv.2104.04095"
  cites: 0
  citedby: 0
  kind: "misc"
  key: "https:-doi.org-10.48550-arxiv.2104.04095"
- title: "An approach to translating Haskell programs to Agda and reasoning about them"
  author:
  - name: "Carr, Harold"
    link: "https://researchr.org/alias/carr%2C-harold"
  - name: "Jenkins, Christa"
    link: "https://researchr.org/alias/jenkins%2C-christa"
  - name: "Moir, Mark"
    link: "https://researchr.org/alias/moir%2C-mark"
  - name: "Miraldo, Victor Cacciari"
    link: "https://researchr.org/alias/miraldo%2C-victor-cacciari"
  - name: "Silva, Lisandra"
    link: "https://researchr.org/alias/silva%2C-lisandra"
  year: "2022"
  doi: "10.48550/ARXIV.2205.08718"
  links:
    "url": "https://arxiv.org/abs/2205.08718"
  researchr: "https://researchr.org/publication/https%3A-doi.org-10.48550-arxiv.2205.08718"
  cites: 0
  citedby: 0
  kind: "misc"
  key: "https:-doi.org-10.48550-arxiv.2205.08718"
- title: "Calculating the Fundamental Group of the Circle in Homotopy Type Theory"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Michael Shulman"
    link: "https://researchr.org/alias/michael-shulman"
  year: "2013"
  doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2013.28"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2013.28"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/LicataS13"
  researchr: "https://researchr.org/publication/LicataS13"
  cites: 0
  citedby: 0
  pages: "223-232"
  booktitle: "lics"
  kind: "inproceedings"
  key: "LicataS13"
- title: "Operational semantics using the partiality monad"
  author:
  - name: "Nils Anders Danielsson"
    link: "https://researchr.org/alias/nils-anders-danielsson"
  year: "2012"
  doi: "http://doi.acm.org/10.1145/2364527.2364546"
  links:
    doi: "http://doi.acm.org/10.1145/2364527.2364546"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/Danielsson12"
  researchr: "https://researchr.org/publication/Danielsson12-0"
  cites: 0
  citedby: 0
  pages: "127-138"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "Danielsson12-0"
- title: "Algebraic Effects Meet Hoare Logic in Cubical Agda"
  author:
  - name: "Donnacha Oisín Kidney"
    link: "https://researchr.org/alias/donnacha-ois%C3%ADn-kidney"
  - name: "Zhixuan Yang"
    link: "https://researchr.org/alias/zhixuan-yang"
  - name: "Nicolas Wu"
    link: "https://researchr.org/alias/nicolas-wu"
  year: "2024"
  month: "January"
  doi: "https://doi.org/10.1145/3632898"
  links:
    doi: "https://doi.org/10.1145/3632898"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/KidneyYW24"
  researchr: "https://researchr.org/publication/KidneyYW24"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "8"
  number: "POPL"
  pages: "1663-1695"
  kind: "article"
  key: "KidneyYW24"
- title: "Safe functional reactive programming through dependent types"
  author:
  - name: "Neil Sculthorpe"
    link: "https://researchr.org/alias/neil-sculthorpe"
  - name: "Henrik Nilsson"
    link: "https://researchr.org/alias/henrik-nilsson"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1596550.1596558"
  links:
    doi: "http://doi.acm.org/10.1145/1596550.1596558"
  tags:
  - "reactive programming"
  - "functional programming"
  - "programming"
  researchr: "https://researchr.org/publication/SculthorpeN09"
  cites: 0
  citedby: 0
  pages: "23-34"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "SculthorpeN09"
- title: "Formalization of Universal Algebra in Agda"
  author:
  - name: "Emmanuel Gunther"
    link: "https://researchr.org/alias/emmanuel-gunther"
  - name: "Alejandro Gadea"
    link: "https://researchr.org/alias/alejandro-gadea"
  - name: "Miguel Pagano"
    link: "https://researchr.org/alias/miguel-pagano"
  year: "2018"
  doi: "https://doi.org/10.1016/j.entcs.2018.10.010"
  links:
    doi: "https://doi.org/10.1016/j.entcs.2018.10.010"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/entcs/GuntherGP18"
  researchr: "https://researchr.org/publication/GuntherGP18"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "338"
  pages: "147-166"
  kind: "article"
  key: "GuntherGP18"
- title: "Impredicative Observational Equality"
  author:
  - name: "Loïc Pujet"
    link: "https://researchr.org/alias/lo%C3%AFc-pujet"
  - name: "Nicolas Tabareau"
    link: "https://researchr.org/alias/nicolas-tabareau"
  year: "2023"
  month: "January"
  doi: "https://doi.org/10.1145/3571739"
  links:
    doi: "https://doi.org/10.1145/3571739"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/PujetT23"
  researchr: "https://researchr.org/publication/PujetT23"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "7"
  number: "POPL"
  pages: "2171-2196"
  kind: "article"
  key: "PujetT23"
- title: "Parsing Mixfix Operators"
  author:
  - name: "Nils Anders Danielsson"
    link: "https://researchr.org/alias/nils-anders-danielsson"
  - name: "Ulf Norell"
    link: "https://researchr.org/alias/ulf-norell"
  year: "2008"
  doi: "http://dx.doi.org/10.1007/978-3-642-24452-0_5"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-24452-0_5"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ifl/DanielssonN08"
  researchr: "https://researchr.org/publication/DanielssonN08"
  cites: 0
  citedby: 0
  pages: "80-99"
  booktitle: "IFL"
  kind: "inproceedings"
  key: "DanielssonN08"
- title: "Unifiers as equivalences: proof-relevant unification of dependently typed data"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2951913.2951917"
  links:
    doi: "http://doi.acm.org/10.1145/2951913.2951917"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/CockxDP16"
  researchr: "https://researchr.org/publication/CockxDP16"
  cites: 0
  citedby: 0
  pages: "270-283"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "CockxDP16"
- title: "Pattern matching without K"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2628136.2628139"
  links:
    doi: "http://doi.acm.org/10.1145/2628136.2628139"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/CockxDP14"
  researchr: "https://researchr.org/publication/CockxDP14"
  cites: 0
  citedby: 0
  pages: "257-268"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "CockxDP14"
- title: "Elaborating dependent (co)pattern matching"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  year: "2018"
  doi: "https://doi.org/10.1145/3236770"
  links:
    doi: "https://doi.org/10.1145/3236770"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/CockxA18"
  researchr: "https://researchr.org/publication/CockxA18"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "2"
  number: "ICFP"
  kind: "article"
  key: "CockxA18"
- title: "Constructions with Non-Recursive Higher Inductive Types"
  author:
  - name: "Nicolai Kraus"
    link: "https://researchr.org/alias/nicolai-kraus"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2933575.2933586"
  links:
    doi: "http://doi.acm.org/10.1145/2933575.2933586"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/Kraus16"
  researchr: "https://researchr.org/publication/Kraus16"
  cites: 0
  citedby: 0
  pages: "595-604"
  booktitle: "lics"
  kind: "inproceedings"
  key: "Kraus16"
- title: "LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs"
  author:
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2012"
  doi: "http://doi.acm.org/10.1145/2103776.2103783"
  links:
    doi: "http://doi.acm.org/10.1145/2103776.2103783"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/plpv/Jeffrey12"
  researchr: "https://researchr.org/publication/Jeffrey12"
  cites: 0
  citedby: 0
  pages: "49-60"
  booktitle: "plpv"
  kind: "inproceedings"
  key: "Jeffrey12"
- title: "Total parser combinators"
  author:
  - name: "Nils Anders Danielsson"
    link: "https://researchr.org/alias/nils-anders-danielsson"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863543.1863585"
  links:
    doi: "http://doi.acm.org/10.1145/1863543.1863585"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/Danielsson10"
  tags:
  - "parsing"
  researchr: "https://researchr.org/publication/Danielsson10"
  cites: 0
  citedby: 0
  pages: "285-296"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "Danielsson10"
- title: "Algebras for weighted search"
  author:
  - name: "Donnacha Oisín Kidney"
    link: "https://researchr.org/alias/donnacha-ois%C3%ADn-kidney"
  - name: "Nicolas Wu"
    link: "https://researchr.org/alias/nicolas-wu"
  year: "2021"
  doi: "https://doi.org/10.1145/3473577"
  links:
    doi: "https://doi.org/10.1145/3473577"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/KidneyW21"
  researchr: "https://researchr.org/publication/KidneyW21"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "5"
  number: "ICFP"
  pages: "1-30"
  kind: "article"
  key: "KidneyW21"
- title: "Static Balance Checking for First-Class Modular Systems of Equations"
  author:
  - name: "John Capper"
    link: "https://researchr.org/alias/john-capper"
  - name: "Henrik Nilsson"
    link: "https://researchr.org/alias/henrik-nilsson"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/978-3-642-22941-1_4"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-22941-1_4"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sfp/CapperN10"
  researchr: "https://researchr.org/publication/CapperN10"
  cites: 0
  citedby: 0
  pages: "50-65"
  booktitle: "sfp"
  kind: "inproceedings"
  key: "CapperN10"
- title: "Reduction monads and their signatures"
  author:
  - name: "Benedikt Ahrens"
    link: "https://researchr.org/alias/benedikt-ahrens"
  - name: "André Hirschowitz"
    link: "https://researchr.org/alias/andr%C3%A9-hirschowitz"
  - name: "Ambroise Lafont"
    link: "https://researchr.org/alias/ambroise-lafont"
  - name: "Marco Maggesi"
    link: "https://researchr.org/alias/marco-maggesi"
  year: "2020"
  doi: "https://doi.org/10.1145/3371099"
  links:
    doi: "https://doi.org/10.1145/3371099"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/AhrensHLM20"
  researchr: "https://researchr.org/publication/AhrensHLM20"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "4"
  number: "POPL"
  kind: "article"
  key: "AhrensHLM20"
- title: "Normalization by Evaluation and Algebraic Effects"
  author:
  - name: "Danel Ahman"
    link: "https://researchr.org/alias/danel-ahman"
  - name: "Sam Staton"
    link: "https://researchr.org/alias/sam-staton"
  year: "2013"
  doi: "http://dx.doi.org/10.1016/j.entcs.2013.09.007"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2013.09.007"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/entcs/AhmanS13"
  researchr: "https://researchr.org/publication/AhmanS13"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "298"
  pages: "51-69"
  kind: "article"
  key: "AhmanS13"
- 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: "Alfa/Agda"
  author:
  - name: "Thierry Coquand"
    link: "https://researchr.org/alias/thierry-coquand"
  year: "2006"
  doi: "http://dx.doi.org/10.1007/11542384_9"
  links:
    doi: "http://dx.doi.org/10.1007/11542384_9"
  researchr: "https://researchr.org/publication/Coquand06"
  cites: 0
  citedby: 0
  pages: "50-54"
  booktitle: "tphol"
  kind: "inproceedings"
  key: "Coquand06"
- title: "Engineering Proof by Reflection in Agda"
  author:
  - name: "Paul van der Walt"
    link: "https://researchr.org/alias/paul-van-der-walt"
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/978-3-642-41582-1_10"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-41582-1_10"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ifl/WaltS12"
  researchr: "https://researchr.org/publication/WaltS12"
  cites: 0
  citedby: 0
  pages: "157-173"
  booktitle: "IFL"
  kind: "inproceedings"
  key: "WaltS12"
- title: "Strong Normalization for the Simply-Typed Lambda Calculus in Constructive Type Theory Using Agda"
  author:
  - name: "Sebastián Urciuoli"
    link: "https://researchr.org/alias/sebasti%C3%A1n-urciuoli"
  - name: "Álvaro Tasistro"
    link: "https://researchr.org/alias/%C3%A1lvaro-tasistro"
  - name: "Nora Szasz"
    link: "https://researchr.org/alias/nora-szasz"
  year: "2020"
  doi: "https://doi.org/10.1016/j.entcs.2020.08.010"
  links:
    doi: "https://doi.org/10.1016/j.entcs.2020.08.010"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lsfa/UrciuoliTS20"
  researchr: "https://researchr.org/publication/UrciuoliTS20"
  cites: 0
  citedby: 0
  pages: "187-203"
  booktitle: "LSFA"
  kind: "inproceedings"
  key: "UrciuoliTS20"
- title: "Well-founded recursion with copatterns and sized types"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Brigitte Pientka"
    link: "https://researchr.org/alias/brigitte-pientka"
  year: "2016"
  doi: "http://dx.doi.org/10.1017/S0956796816000022"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796816000022"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/0001P16"
  researchr: "https://researchr.org/publication/0001P16-8"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "26"
  kind: "article"
  key: "0001P16-8"
- title: "Toward SMT-Based Refinement Types in Agda"
  author:
  - name: "Shen, Gan"
    link: "https://researchr.org/alias/shen%2C-gan"
  - name: "Kuper, Lindsey"
    link: "https://researchr.org/alias/kuper%2C-lindsey"
  year: "2021"
  doi: "10.48550/ARXIV.2110.05771"
  links:
    "url": "https://arxiv.org/abs/2110.05771"
  researchr: "https://researchr.org/publication/https%3A-doi.org-10.48550-arxiv.2110.05771"
  cites: 0
  citedby: 0
  kind: "misc"
  key: "https:-doi.org-10.48550-arxiv.2110.05771"
- title: "Refinement types and computational duality"
  author:
  - name: "Noam Zeilberger"
    link: "https://researchr.org/alias/noam-zeilberger"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1481848.1481852"
  links:
    doi: "http://doi.acm.org/10.1145/1481848.1481852"
  tags:
  - "refinement"
  researchr: "https://researchr.org/publication/Zeilberger09"
  cites: 0
  citedby: 0
  pages: "15-26"
  booktitle: "plpv"
  kind: "inproceedings"
  key: "Zeilberger09"
- title: "Translating Proofs from an Impredicative Type System to a Predicative One"
  author:
  - name: "Thiago Felicissimo"
    link: "https://researchr.org/alias/thiago-felicissimo"
  - name: "Frédéric Blanqui"
    link: "https://researchr.org/alias/fr%C3%A9d%C3%A9ric-blanqui"
  - name: "Ashish Kumar Barnawal"
    link: "https://researchr.org/alias/ashish-kumar-barnawal"
  year: "2023"
  doi: "https://doi.org/10.4230/LIPIcs.CSL.2023.19"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.CSL.2023.19"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/FelicissimoBB23"
  researchr: "https://researchr.org/publication/FelicissimoBB23"
  cites: 0
  citedby: 0
  booktitle: "csl"
  kind: "inproceedings"
  key: "FelicissimoBB23"
- title: "Generic level polymorphic n-ary functions"
  author:
  - name: "Guillaume Allais"
    link: "https://researchr.org/alias/guillaume-allais"
  year: "2019"
  doi: "https://doi.org/10.1145/3331554.3342604"
  links:
    doi: "https://doi.org/10.1145/3331554.3342604"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/Allais19"
  researchr: "https://researchr.org/publication/Allais19"
  cites: 0
  citedby: 0
  pages: "14-26"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "Allais19"
- title: "Quotienting the delay monad by weak bisimilarity"
  author:
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  year: "2019"
  doi: "https://doi.org/10.1017/S0960129517000184"
  links:
    doi: "https://doi.org/10.1017/S0960129517000184"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/mscs/ChapmanUV19"
  researchr: "https://researchr.org/publication/ChapmanUV19"
  cites: 0
  citedby: 0
  journal: "mscs"
  volume: "29"
  number: "1"
  pages: "67-92"
  kind: "article"
  key: "ChapmanUV19"
- title: "Testing versus proving in climate impact research"
  author:
  - name: "Cezar Ionescu"
    link: "https://researchr.org/alias/cezar-ionescu"
  - name: "Patrik Jansson"
    link: "https://researchr.org/alias/patrik-jansson"
  year: "2011"
  doi: "http://dx.doi.org/10.4230/LIPIcs.TYPES.2011.41"
  links:
    doi: "http://dx.doi.org/10.4230/LIPIcs.TYPES.2011.41"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/types/IonescuJ11"
  researchr: "https://researchr.org/publication/IonescuJ11"
  cites: 0
  citedby: 0
  pages: "41-54"
  booktitle: "TYPES"
  kind: "inproceedings"
  key: "IonescuJ11"
- title: "A foundation for GADTs and inductive families: dependent polynomial functor approach"
  author:
  - name: "Makoto Hamana"
    link: "https://researchr.org/alias/makoto-hamana"
  - name: "Marcelo P. Fiore"
    link: "https://researchr.org/alias/marcelo-p.-fiore"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/2036918.2036927"
  links:
    doi: "http://doi.acm.org/10.1145/2036918.2036927"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/HamanaF11"
  researchr: "https://researchr.org/publication/HamanaF11"
  cites: 0
  citedby: 0
  pages: "59-70"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "HamanaF11"
- title: "Adjoint Logic with a 2-Category of Modes"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Michael Shulman"
    link: "https://researchr.org/alias/michael-shulman"
  year: "2016"
  doi: "http://dx.doi.org/10.1007/978-3-319-27683-0_16"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-27683-0_16"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lfcs/LicataS16"
  researchr: "https://researchr.org/publication/LicataS16"
  cites: 0
  citedby: 0
  pages: "219-235"
  booktitle: "lfcs"
  kind: "inproceedings"
  key: "LicataS16"
- title: "Lightweight semiformal time complexity analysis for purely functional data structures"
  author:
  - name: "Nils Anders Danielsson"
    link: "https://researchr.org/alias/nils-anders-danielsson"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1328438.1328457"
  links:
    doi: "http://doi.acm.org/10.1145/1328438.1328457"
  tags:
  - "analysis"
  - "data-flow analysis"
  researchr: "https://researchr.org/publication/Danielsson08"
  cites: 0
  citedby: 0
  pages: "133-144"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "Danielsson08"
- title: "Another Look at Function Domains"
  author:
  - name: "Ana Bove"
    link: "https://researchr.org/alias/ana-bove"
  year: "2009"
  doi: "http://dx.doi.org/10.1016/j.entcs.2009.07.084"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2009.07.084"
  researchr: "https://researchr.org/publication/Bove09"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "249"
  pages: "61-74"
  kind: "article"
  key: "Bove09"
- title: "Programming assurance cases in Agda"
  author:
  - name: "Makoto Takeyama"
    link: "https://researchr.org/alias/makoto-takeyama"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/2034773.2034794"
  links:
    doi: "http://doi.acm.org/10.1145/2034773.2034794"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/Takeyama11"
  researchr: "https://researchr.org/publication/Takeyama11"
  cites: 0
  citedby: 0
  pages: "142"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "Takeyama11"
- title: "A Type Theoretic Specification of Partial Evaluation"
  author:
  - name: "Kenichi Asai"
    link: "https://researchr.org/alias/kenichi-asai"
  - name: "Luminous Fennell"
    link: "https://researchr.org/alias/luminous-fennell"
  - name: "Peter Thiemann"
    link: "https://researchr.org/alias/peter-thiemann"
  - name: "Yang Zhang"
    link: "https://researchr.org/alias/yang-zhang"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2643135.2643146"
  links:
    doi: "http://doi.acm.org/10.1145/2643135.2643146"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/AsaiFTZ14"
  researchr: "https://researchr.org/publication/AsaiFTZ14"
  cites: 0
  citedby: 0
  pages: "57-68"
  booktitle: "ppdp"
  kind: "inproceedings"
  key: "AsaiFTZ14"
- title: "Dependently typed programming with finite sets"
  author:
  - name: "Denis Firsov"
    link: "https://researchr.org/alias/denis-firsov"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  year: "2015"
  doi: "http://doi.acm.org/10.1145/2808098.2808102"
  links:
    doi: "http://doi.acm.org/10.1145/2808098.2808102"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/FirsovU15"
  researchr: "https://researchr.org/publication/FirsovU15-0"
  cites: 0
  citedby: 0
  pages: "33-44"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "FirsovU15-0"
- title: "A predicate transformer semantics for effects (functional pearl)"
  author:
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  - name: "Tim Baanen"
    link: "https://researchr.org/alias/tim-baanen"
  year: "2019"
  doi: "https://doi.org/10.1145/3341707"
  links:
    doi: "https://doi.org/10.1145/3341707"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/SwierstraB19"
  researchr: "https://researchr.org/publication/SwierstraB19"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "3"
  number: "ICFP"
  kind: "article"
  key: "SwierstraB19"
- title: "Three equivalent ordinal notation systems in cubical Agda"
  author:
  - name: "Fredrik Nordvall Forsberg"
    link: "https://researchr.org/alias/fredrik-nordvall-forsberg"
  - name: "Chuangjie Xu"
    link: "https://researchr.org/alias/chuangjie-xu"
  - name: "Neil Ghani"
    link: "https://researchr.org/alias/neil-ghani"
  year: "2020"
  doi: "https://doi.org/10.1145/3372885.3373835"
  links:
    doi: "https://doi.org/10.1145/3372885.3373835"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/ForsbergXG20"
  researchr: "https://researchr.org/publication/ForsbergXG20"
  cites: 0
  citedby: 0
  pages: "172-185"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "ForsbergXG20"
- title: "Teaching automated reasoning and formally verified functional programming in Agda and Isabelle/HOL"
  author:
  - name: "From, Asta Halkjær "
    link: "https://researchr.org/alias/from%2C-asta-halkj%C3%A6r"
  - name: "Villadsen, Jørgen "
    link: "https://researchr.org/alias/villadsen%2C-j%C3%B8rgen"
  year: "2021"
  researchr: "https://researchr.org/publication/from2021teaching"
  cites: 0
  citedby: 0
  pages: "1-20"
  booktitle: "10th International Workshop on Trends in Functional Programming in Education (TFPIE 2021)--Presentation Only/Online Papers"
  kind: "inproceedings"
  key: "from2021teaching"
- title: "Programming language foundations in Agda"
  author:
  - name: "Wen Kokke"
    link: "https://researchr.org/alias/wen-kokke"
  - name: "Jeremy G. Siek"
    link: "https://researchr.org/alias/jeremy-g.-siek"
  - name: "Philip Wadler"
    link: "https://researchr.org/alias/philip-wadler"
  year: "2020"
  doi: "https://doi.org/10.1016/j.scico.2020.102440"
  links:
    doi: "https://doi.org/10.1016/j.scico.2020.102440"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/scp/KokkeSW20"
  researchr: "https://researchr.org/publication/KokkeSW20"
  cites: 0
  citedby: 0
  journal: "SCP"
  volume: "194"
  pages: "102440"
  kind: "article"
  key: "KokkeSW20"
- title: "Hazelnut: a bidirectionally typed structure editor calculus"
  author:
  - name: "Cyrus Omar"
    link: "https://researchr.org/alias/cyrus-omar"
  - name: "Ian Voysey"
    link: "https://researchr.org/alias/ian-voysey"
  - name: "Michael Hilton"
    link: "https://researchr.org/alias/michael-hilton"
  - name: "Jonathan Aldrich"
    link: "https://researchr.org/alias/jonathan-aldrich"
  - name: "Matthew A. Hammer"
    link: "https://researchr.org/alias/matthew-a.-hammer"
  year: "2017"
  doi: "http://dl.acm.org/citation.cfm?id=3009900"
  links:
    doi: "http://dl.acm.org/citation.cfm?id=3009900"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/OmarVHAH17"
  researchr: "https://researchr.org/publication/OmarVHAH17"
  cites: 0
  citedby: 0
  pages: "86-99"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "OmarVHAH17"
- title: "Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda"
  author:
  - name: "Andre Knispel"
    link: "https://researchr.org/alias/andre-knispel"
  - name: "Orestis Melkonian"
    link: "https://researchr.org/alias/orestis-melkonian"
  - name: "James Chapman 0001"
    link: "https://researchr.org/alias/james-chapman-0001"
  - name: "Alasdair Hill"
    link: "https://researchr.org/alias/alasdair-hill"
  - name: "Joosep Jääger"
    link: "https://researchr.org/alias/joosep-j%C3%A4%C3%A4ger"
  - name: "William J. DeMeo"
    link: "https://researchr.org/alias/william-j.-demeo"
  - name: "Ulf Norell"
    link: "https://researchr.org/alias/ulf-norell"
  year: "2024"
  doi: "https://doi.org/10.4230/OASIcs.FMBC.2024.2"
  links:
    doi: "https://doi.org/10.4230/OASIcs.FMBC.2024.2"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fmbc/KnispelM0HJDN24"
  researchr: "https://researchr.org/publication/KnispelM0HJDN24"
  cites: 0
  citedby: 0
  booktitle: "fmbc"
  kind: "inproceedings"
  key: "KnispelM0HJDN24"
- title: "Turing-Completeness Totally Free"
  author:
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  year: "2015"
  doi: "http://dx.doi.org/10.1007/978-3-319-19797-5_13"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-19797-5_13"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/mpc/McBride15"
  researchr: "https://researchr.org/publication/McBride15"
  cites: 0
  citedby: 0
  pages: "257-275"
  booktitle: "mpc"
  kind: "inproceedings"
  key: "McBride15"
- title: "Forward build systems, formally"
  author:
  - name: "Sarah Spall"
    link: "https://researchr.org/alias/sarah-spall"
  - name: "Neil Mitchell"
    link: "https://researchr.org/alias/neil-mitchell"
  - name: "Sam Tobin-Hochstadt"
    link: "https://researchr.org/alias/sam-tobin-hochstadt"
  year: "2022"
  doi: "https://doi.org/10.1145/3497775.3503687"
  links:
    doi: "https://doi.org/10.1145/3497775.3503687"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/SpallMT22"
  researchr: "https://researchr.org/publication/SpallMT22"
  cites: 0
  citedby: 0
  pages: "130-142"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "SpallMT22"
- title: "The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard Interpretation"
  author:
  - name: "Martín Hötzel Escardó"
    link: "https://researchr.org/alias/mart%C3%ADn-h%C3%B6tzel-escard%C3%B3"
  - name: "Chuangjie Xu"
    link: "https://researchr.org/alias/chuangjie-xu"
  year: "2015"
  doi: "http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.153"
  links:
    doi: "http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.153"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tlca/EscardoX15"
  researchr: "https://researchr.org/publication/EscardoX15"
  cites: 0
  citedby: 0
  pages: "153-164"
  booktitle: "tlca"
  kind: "inproceedings"
  key: "EscardoX15"
- title: "Modal μ-Calculus for Free in Agda"
  author:
  - name: "Ivan Todorov"
    link: "https://researchr.org/alias/ivan-todorov"
  - name: "Casper Bach Poulsen"
    link: "https://researchr.org/alias/casper-bach-poulsen"
  year: "2024"
  doi: "https://doi.org/10.1145/3678000.3678202"
  links:
    doi: "https://doi.org/10.1145/3678000.3678202"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tyde/TodorovP24"
  researchr: "https://researchr.org/publication/TodorovP24"
  cites: 0
  citedby: 0
  pages: "16-28"
  booktitle: "tyde"
  kind: "inproceedings"
  key: "TodorovP24"
- title: "Functional Pearl: Folding Polynomials of Polynomials"
  author:
  - name: "Chen-Mou Cheng"
    link: "https://researchr.org/alias/chen-mou-cheng"
  - name: "Ruey-Lin Hsu"
    link: "https://researchr.org/alias/ruey-lin-hsu"
  - name: "Shin-Cheng Mu"
    link: "https://researchr.org/alias/shin-cheng-mu"
  year: "2018"
  doi: "https://doi.org/10.1007/978-3-319-90686-7_5"
  links:
    doi: "https://doi.org/10.1007/978-3-319-90686-7_5"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/flops/ChengHM18"
  researchr: "https://researchr.org/publication/ChengHM18"
  cites: 0
  citedby: 0
  pages: "68-83"
  booktitle: "FLOPS"
  kind: "inproceedings"
  key: "ChengHM18"
- title: "Dependent Types for Distributed Arrays"
  author:
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  year: "2008"
  links:
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sfp/SwierstraA08"
  researchr: "https://researchr.org/publication/SwierstraA08"
  cites: 0
  citedby: 0
  pages: "17-32"
  booktitle: "sfp"
  kind: "inproceedings"
  key: "SwierstraA08"
- title: "When Is a Container a Comonad?"
  author:
  - name: "Danel Ahman"
    link: "https://researchr.org/alias/danel-ahman"
  - name: "James Chapman"
    link: "https://researchr.org/alias/james-chapman"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/978-3-642-28729-9_5"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-28729-9_5"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fossacs/AhmanCU12"
  researchr: "https://researchr.org/publication/AhmanCU12"
  cites: 0
  citedby: 0
  pages: "74-88"
  booktitle: "fossacs"
  kind: "inproceedings"
  key: "AhmanCU12"
- title: "Plausible sealing for gradual parametricity"
  author:
  - name: "Elizabeth Labrada"
    link: "https://researchr.org/alias/elizabeth-labrada"
  - name: "Matías Toro"
    link: "https://researchr.org/alias/mat%C3%ADas-toro"
  - name: "Éric Tanter"
    link: "https://researchr.org/alias/%C3%A9ric-tanter"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2022"
  doi: "https://doi.org/10.1145/3527314"
  links:
    doi: "https://doi.org/10.1145/3527314"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/LabradaTTD22"
  researchr: "https://researchr.org/publication/LabradaTTD22"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "6"
  number: "OOPSLA"
  pages: "1-28"
  kind: "article"
  key: "LabradaTTD22"
- title: "What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift Have in Common"
  author:
  - name: "Martín Escardó"
    link: "https://researchr.org/alias/mart%C3%ADn-escard%C3%B3"
  - name: "Paulo Oliva"
    link: "https://researchr.org/alias/paulo-oliva"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863597.1863605"
  links:
    doi: "http://doi.acm.org/10.1145/1863597.1863605"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/EscardoO10"
  researchr: "https://researchr.org/publication/EscardoO10-1"
  cites: 0
  citedby: 0
  pages: "21-32"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "EscardoO10-1"
- title: "Cubical synthetic homotopy theory"
  author:
  - name: "Anders Mörtberg"
    link: "https://researchr.org/alias/anders-m%C3%B6rtberg"
  - name: "Loïc Pujet"
    link: "https://researchr.org/alias/lo%C3%AFc-pujet"
  year: "2020"
  doi: "https://doi.org/10.1145/3372885.3373825"
  links:
    doi: "https://doi.org/10.1145/3372885.3373825"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/MortbergP20"
  researchr: "https://researchr.org/publication/MortbergP20"
  cites: 0
  citedby: 0
  pages: "158-171"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "MortbergP20"
- title: "How to do proofs: practically proving properties about effectful programs' results (functional pearl)"
  author:
  - name: "Koen Jacobs"
    link: "https://researchr.org/alias/koen-jacobs"
  - name: "Andreas Nuyts"
    link: "https://researchr.org/alias/andreas-nuyts"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2019"
  doi: "https://doi.org/10.1145/3331554.3342603"
  links:
    doi: "https://doi.org/10.1145/3331554.3342603"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/JacobsND19"
  researchr: "https://researchr.org/publication/JacobsND19"
  cites: 0
  citedby: 0
  pages: "1-13"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "JacobsND19"
- title: "Deferring the details and deriving programs"
  author:
  - name: "Liam O'Connor"
    link: "https://researchr.org/alias/liam-o%27connor"
  year: "2019"
  doi: "https://doi.org/10.1145/3331554.3342605"
  links:
    doi: "https://doi.org/10.1145/3331554.3342605"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/OConnor19"
  researchr: "https://researchr.org/publication/OConnor19"
  cites: 0
  citedby: 0
  pages: "27-39"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "OConnor19"
- title: "Computing Cohomology Rings in Cubical Agda"
  author:
  - name: "Thomas Lamiaux"
    link: "https://researchr.org/alias/thomas-lamiaux"
  - name: "Axel Ljungström"
    link: "https://researchr.org/alias/axel-ljungstr%C3%B6m"
  - name: "Anders Mörtberg"
    link: "https://researchr.org/alias/anders-m%C3%B6rtberg"
  year: "2023"
  doi: "https://doi.org/10.1145/3573105.3575677"
  links:
    doi: "https://doi.org/10.1145/3573105.3575677"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/LamiauxLM23"
  researchr: "https://researchr.org/publication/LamiauxLM23"
  cites: 0
  citedby: 0
  pages: "239-252"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "LamiauxLM23"
- title: "Interactive programming in Agda - Objects and graphical user interfaces"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Stephan Adelsberger"
    link: "https://researchr.org/alias/stephan-adelsberger"
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  year: "2017"
  doi: "http://dx.doi.org/10.1017/S0956796816000319"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796816000319"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/AbelAS17"
  researchr: "https://researchr.org/publication/AbelAS17"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "27"
  kind: "article"
  key: "AbelAS17"
- title: "Multiple Conclusion Linear Logic: Cut Elimination and More"
  author:
  - name: "Harley Eades III"
    link: "https://researchr.org/alias/harley-eades-iii"
  - name: "Valeria de Paiva"
    link: "https://researchr.org/alias/valeria-de-paiva"
  year: "2016"
  doi: "http://dx.doi.org/10.1007/978-3-319-27683-0_7"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-27683-0_7"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lfcs/EadesP16"
  researchr: "https://researchr.org/publication/EadesP16"
  cites: 0
  citedby: 0
  pages: "90-105"
  booktitle: "lfcs"
  kind: "inproceedings"
  key: "EadesP16"
- title: "An Agda Formalization of Üresin and Dubois' Asynchronous Fixed-Point Theory"
  author:
  - name: "Ran Zmigrod"
    link: "https://researchr.org/alias/ran-zmigrod"
  - name: "Matthew L. Daggitt"
    link: "https://researchr.org/alias/matthew-l.-daggitt"
  - name: "Timothy G. Griffin"
    link: "https://researchr.org/alias/timothy-g.-griffin"
  year: "2018"
  doi: "https://doi.org/10.1007/978-3-319-94821-8_37"
  links:
    doi: "https://doi.org/10.1007/978-3-319-94821-8_37"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/ZmigrodDG18"
  researchr: "https://researchr.org/publication/ZmigrodDG18"
  cites: 0
  citedby: 0
  pages: "623-639"
  booktitle: "itp"
  kind: "inproceedings"
  key: "ZmigrodDG18"
- title: "A computational interpretation of compact closed categories: reversible programming with negative and fractional types"
  author:
  - name: "Chao-Hong Chen"
    link: "https://researchr.org/alias/chao-hong-chen"
  - name: "Amr Sabry"
    link: "https://researchr.org/alias/amr-sabry"
  year: "2021"
  doi: "https://doi.org/10.1145/3434290"
  links:
    doi: "https://doi.org/10.1145/3434290"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/ChenS21"
  researchr: "https://researchr.org/publication/ChenS21-1"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "5"
  number: "POPL"
  pages: "1-29"
  kind: "article"
  key: "ChenS21-1"
- title: "Embedding polymorphic dynamic typing"
  author:
  - name: "Thomas van Noort"
    link: "https://researchr.org/alias/thomas-van-noort"
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  - name: "Peter Achten"
    link: "https://researchr.org/alias/peter-achten"
  - name: "Rinus Plasmeijer"
    link: "https://researchr.org/alias/rinus-plasmeijer"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/2036918.2036923"
  links:
    doi: "http://doi.acm.org/10.1145/2036918.2036923"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/NoortSAP11"
  researchr: "https://researchr.org/publication/NoortSAP11"
  cites: 0
  citedby: 0
  pages: "25-36"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "NoortSAP11"
- title: "Asynchronous effects"
  author:
  - name: "Danel Ahman"
    link: "https://researchr.org/alias/danel-ahman"
  - name: "Matija Pretnar"
    link: "https://researchr.org/alias/matija-pretnar"
  year: "2021"
  doi: "https://doi.org/10.1145/3434305"
  links:
    doi: "https://doi.org/10.1145/3434305"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/AhmanP21"
  researchr: "https://researchr.org/publication/AhmanP21"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "5"
  number: "POPL"
  pages: "1-28"
  kind: "article"
  key: "AhmanP21"
- title: "Mechanised Relation-Algebraic Order Theory in Ordered Categories without Meets"
  author:
  - name: "Musa Al-hassy"
    link: "https://researchr.org/alias/musa-al-hassy"
  - name: "Wolfram Kahl"
    link: "https://researchr.org/alias/wolfram-kahl"
  year: "2015"
  doi: "http://dx.doi.org/10.1007/978-3-319-24704-5_10"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-24704-5_10"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/RelMiCS/Al-hassyK15"
  researchr: "https://researchr.org/publication/Al-hassyK15"
  cites: 0
  citedby: 0
  pages: "151-168"
  booktitle: "RelMiCS"
  kind: "inproceedings"
  key: "Al-hassyK15"
- title: "A constructive manifestation of the Kleene-Kreisel continuous functionals"
  author:
  - name: "Martín Escardó"
    link: "https://researchr.org/alias/mart%C3%ADn-escard%C3%B3"
  - name: "Chuangjie Xu"
    link: "https://researchr.org/alias/chuangjie-xu"
  year: "2016"
  doi: "http://dx.doi.org/10.1016/j.apal.2016.04.011"
  links:
    doi: "http://dx.doi.org/10.1016/j.apal.2016.04.011"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/apal/EscardoX16"
  researchr: "https://researchr.org/publication/EscardoX16"
  cites: 0
  citedby: 0
  journal: "APAL"
  volume: "167"
  number: "9"
  pages: "770-793"
  kind: "article"
  key: "EscardoX16"
- title: "Modularising inductive families"
  author:
  - name: "Hsiang-Shang Ko"
    link: "https://researchr.org/alias/hsiang-shang-ko"
  - name: "Jeremy Gibbons"
    link: "https://researchr.org/alias/jeremy-gibbons"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/2036918.2036921"
  links:
    doi: "http://doi.acm.org/10.1145/2036918.2036921"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/KoG11"
  researchr: "https://researchr.org/publication/KoG11"
  cites: 0
  citedby: 0
  pages: "13-24"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "KoG11"
- title: "LibNDT: Towards a Formal Library on Spreadable Properties over Linked Nested Datatypes"
  author:
  - name: "Mathieu Montin"
    link: "https://researchr.org/alias/mathieu-montin"
  - name: "Amélie Ledein"
    link: "https://researchr.org/alias/am%C3%A9lie-ledein"
  - name: "Catherine Dubois"
    link: "https://researchr.org/alias/catherine-dubois"
  year: "2022"
  month: "jun"
  doi: "10.4204/eptcs.360.2"
  links:
    "url": "https://doi.org/10.4204%2Feptcs.360.2"
  researchr: "https://researchr.org/publication/Montin2022"
  cites: 0
  citedby: 0
  journal: "Electronic Proceedings in Theoretical Computer Science"
  volume: "360"
  pages: "27-44"
  kind: "article"
  key: "Montin2022"
- title: "Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study"
  author:
  - name: "Jacques Carette"
    link: "https://researchr.org/alias/jacques-carette"
  - name: "William M. Farmer"
    link: "https://researchr.org/alias/william-m.-farmer"
  year: "2017"
  doi: "https://doi.org/10.1007/978-3-319-62075-6_2"
  links:
    doi: "https://doi.org/10.1007/978-3-319-62075-6_2"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/mkm/CaretteF17"
  researchr: "https://researchr.org/publication/CaretteF17"
  cites: 0
  citedby: 0
  pages: "9-24"
  booktitle: "mkm"
  kind: "inproceedings"
  key: "CaretteF17"
- title: "A Tool for Automated Theorem Proving in Agda"
  author:
  - name: "Fredrik Lindblad"
    link: "https://researchr.org/alias/fredrik-lindblad"
  - name: "Marcin Benke"
    link: "https://researchr.org/alias/marcin-benke"
  year: "2004"
  doi: "http://dx.doi.org/10.1007/11617990_10"
  links:
    doi: "http://dx.doi.org/10.1007/11617990_10"
  researchr: "https://researchr.org/publication/LindbladB04"
  cites: 0
  citedby: 0
  pages: "154-169"
  booktitle: "TYPES"
  kind: "inproceedings"
  key: "LindbladB04"
- title: "A library for polymorphic dynamic typing"
  author:
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  - name: "Thomas van Noort"
    link: "https://researchr.org/alias/thomas-van-noort"
  year: "2013"
  doi: "http://dx.doi.org/10.1017/S0956796813000063"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796813000063"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/SwierstraN13"
  researchr: "https://researchr.org/publication/SwierstraN13"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "23"
  number: "3"
  pages: "229-248"
  kind: "article"
  key: "SwierstraN13"
- title: "Parametricity and dependent types"
  author:
  - name: "Jean-Philippe Bernardy"
    link: "http://www.chalmers.se/cse/EN/people/bernardy-jean-philippe"
  - name: "Patrik Jansson"
    link: "http://www.chalmers.se/cse/EN/people/jansson-patrik"
  - name: "Ross Paterson"
    link: "http://www.soi.city.ac.uk/~ross/"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863543.1863592"
  abstract: "Reynolds' abstraction theorem shows how a typing judgement in System F can be translated into a relational statement (in second order predicate logic) about inhabitants of the type. We expose a similar result, where terms, types, and their relations are expressed in a single typed lambda calculus (a pure type system). Working within a single system dispenses the need for an interpretation layer, allowing for an unusually simple presentation. While the unification puts some constraints on the type system (which we spell out), the result applies to many interesting cases, including dependently-typed ones."
  links:
    doi: "http://doi.acm.org/10.1145/1863543.1863592"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/BernardyJP10"
  tags:
  - "translation"
  - "constraints"
  - "type system"
  - "logic"
  - "abstraction"
  researchr: "https://researchr.org/publication/BernardyJP10"
  cites: 0
  citedby: 0
  pages: "345-356"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "BernardyJP10"
- title: "Interactive programming with dependent types"
  author:
  - name: "Ulf Norell"
    link: "https://researchr.org/alias/ulf-norell"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2500365.2500610"
  links:
    doi: "http://doi.acm.org/10.1145/2500365.2500610"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/Norell13"
  researchr: "https://researchr.org/publication/Norell13"
  cites: 0
  citedby: 0
  pages: "1-2"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "Norell13"
- title: "A Cubical Approach to Synthetic Homotopy Theory"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Guillaume Brunerie"
    link: "https://researchr.org/alias/guillaume-brunerie"
  year: "2015"
  doi: "http://dx.doi.org/10.1109/LICS.2015.19"
  links:
    doi: "http://dx.doi.org/10.1109/LICS.2015.19"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/LicataB15"
  researchr: "https://researchr.org/publication/LicataB15"
  cites: 0
  citedby: 0
  pages: "92-103"
  booktitle: "lics"
  kind: "inproceedings"
  key: "LicataB15"
- title: "Decomposing the Univalence Axiom"
  author:
  - name: "Ian Orton"
    link: "https://researchr.org/alias/ian-orton"
  - name: "Andrew M. Pitts"
    link: "https://researchr.org/alias/andrew-m.-pitts"
  year: "2017"
  doi: "https://doi.org/10.4230/LIPIcs.TYPES.2017.6"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.TYPES.2017.6"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/types/OrtonP17"
  researchr: "https://researchr.org/publication/OrtonP17-0"
  cites: 0
  citedby: 0
  booktitle: "TYPES"
  kind: "inproceedings"
  key: "OrtonP17-0"
- title: "Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics"
  author:
  - name: "Martín Escardó"
    link: "https://researchr.org/alias/mart%C3%ADn-escard%C3%B3"
  year: "2013"
  doi: "http://projecteuclid.org/euclid.jsl/1389032274"
  links:
    doi: "http://projecteuclid.org/euclid.jsl/1389032274"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jsyml/Escardo13"
  researchr: "https://researchr.org/publication/Escardo13-1"
  cites: 0
  citedby: 0
  journal: "JSYML"
  volume: "78"
  number: "3"
  pages: "764-784"
  kind: "article"
  key: "Escardo13-1"
- title: "Functional reactive types"
  author:
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2603088.2603106"
  links:
    doi: "http://doi.acm.org/10.1145/2603088.2603106"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/Jeffrey14"
  researchr: "https://researchr.org/publication/Jeffrey14"
  cites: 0
  citedby: 0
  pages: "54"
  booktitle: "csl"
  kind: "inproceedings"
  key: "Jeffrey14"
- title: "Towards an Extrinsic Formalization of Featherweight Java in Agda"
  author:
  - name: "Samuel da Silva Feitosa"
    link: "https://researchr.org/alias/samuel-da-silva-feitosa"
  - name: "Rodrigo Geraldo Ribeiro"
    link: "https://researchr.org/alias/rodrigo-geraldo-ribeiro"
  - name: "André Rauber Du Bois"
    link: "https://researchr.org/alias/andr%C3%A9-rauber-du-bois"
  year: "2021"
  doi: "https://doi.org/10.19153/cleiej.24.3.3"
  links:
    doi: "https://doi.org/10.19153/cleiej.24.3.3"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/cleiej/FeitosaRB21"
  researchr: "https://researchr.org/publication/FeitosaRB21"
  cites: 0
  citedby: 0
  journal: "cleiej"
  volume: "24"
  number: "3"
  kind: "article"
  key: "FeitosaRB21"
- title: "Relational algebraic ornaments"
  author:
  - name: "Hsiang-Shang Ko"
    link: "https://researchr.org/alias/hsiang-shang-ko"
  - name: "Jeremy Gibbons"
    link: "https://researchr.org/alias/jeremy-gibbons"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2502409.2502413"
  links:
    doi: "http://doi.acm.org/10.1145/2502409.2502413"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/KoG13"
  researchr: "https://researchr.org/publication/KoG13-1"
  cites: 0
  citedby: 0
  pages: "37-48"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "KoG13-1"
- title: "Modular type-safety proofs in Agda"
  author:
  - name: "Christopher Schwaab"
    link: "https://researchr.org/alias/christopher-schwaab"
  - name: "Jeremy G. Siek"
    link: "http://homes.soic.indiana.edu/jsiek/"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2428116.2428120"
  links:
    doi: "http://doi.acm.org/10.1145/2428116.2428120"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/plpv/SchwaabS13"
  researchr: "https://researchr.org/publication/SchwaabS13"
  cites: 0
  citedby: 0
  pages: "3-12"
  booktitle: "plpv"
  kind: "inproceedings"
  key: "SchwaabS13"
- title: "Code Generation for Higher Inductive Types - A Study in Agda Metaprogramming"
  author:
  - name: "Paventhan Vivekanandan"
    link: "https://researchr.org/alias/paventhan-vivekanandan"
  year: "2018"
  doi: "https://doi.org/10.1007/978-3-030-16202-3_2"
  links:
    doi: "https://doi.org/10.1007/978-3-030-16202-3_2"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/wflp/Vivekanandan18"
  researchr: "https://researchr.org/publication/Vivekanandan18-0"
  cites: 0
  citedby: 0
  pages: "18-35"
  booktitle: "wflp"
  kind: "inproceedings"
  key: "Vivekanandan18-0"
- title: "A Relaxation of Üresin and Dubois' Asynchronous Fixed-Point Theory in Agda"
  author:
  - name: "Matthew L. Daggitt"
    link: "https://researchr.org/alias/matthew-l.-daggitt"
  - name: "Ran Zmigrod"
    link: "https://researchr.org/alias/ran-zmigrod"
  - name: "Timothy G. Griffin"
    link: "https://researchr.org/alias/timothy-g.-griffin"
  year: "2020"
  doi: "https://doi.org/10.1007/s10817-019-09536-w"
  links:
    doi: "https://doi.org/10.1007/s10817-019-09536-w"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jar/DaggittZG20"
  researchr: "https://researchr.org/publication/DaggittZG20"
  cites: 0
  citedby: 0
  journal: "JAR"
  volume: "64"
  number: "5"
  pages: "857-877"
  kind: "article"
  key: "DaggittZG20"
- title: "Normalization for fitch-style modal calculi"
  author:
  - name: "Nachiappan Valliappan"
    link: "https://researchr.org/alias/nachiappan-valliappan"
  - name: "Fabian Ruch"
    link: "https://researchr.org/alias/fabian-ruch"
  - name: "Carlos Tomé Cortiñas"
    link: "https://researchr.org/alias/carlos-tom%C3%A9-corti%C3%B1as"
  year: "2022"
  doi: "https://doi.org/10.1145/3547649"
  links:
    doi: "https://doi.org/10.1145/3547649"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/ValliappanRC22"
  researchr: "https://researchr.org/publication/ValliappanRC22"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "6"
  number: "ICFP"
  pages: "772-798"
  kind: "article"
  key: "ValliappanRC22"
- title: "How to keep your neighbours in order"
  author:
  - name: "Conor Thomas McBride"
    link: "https://researchr.org/alias/conor-thomas-mcbride"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2628136.2628163"
  links:
    doi: "http://doi.acm.org/10.1145/2628136.2628163"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/McBride14"
  researchr: "https://researchr.org/publication/McBride14-2"
  cites: 0
  citedby: 0
  pages: "297-309"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "McBride14-2"
- title: "Nameless, painless"
  author:
  - name: "Nicolas Pouillard"
    link: "https://researchr.org/alias/nicolas-pouillard"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/2034773.2034817"
  links:
    doi: "http://doi.acm.org/10.1145/2034773.2034817"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/Pouillard11"
  researchr: "https://researchr.org/publication/Pouillard11"
  cites: 0
  citedby: 0
  pages: "320-332"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "Pouillard11"
- title: "Definitional proof-irrelevance without K"
  author:
  - name: "Gaëtan Gilbert"
    link: "https://researchr.org/alias/ga%C3%ABtan-gilbert"
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Matthieu Sozeau"
    link: "https://researchr.org/alias/matthieu-sozeau"
  - name: "Nicolas Tabareau"
    link: "https://researchr.org/alias/nicolas-tabareau"
  year: "2019"
  doi: "https://dl.acm.org/citation.cfm?id=3290316"
  links:
    doi: "https://dl.acm.org/citation.cfm?id=3290316"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/GilbertCST19"
  researchr: "https://researchr.org/publication/GilbertCST19"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "3"
  kind: "article"
  key: "GilbertCST19"
- title: "The Agda Universal Algebra Library, Part 2: Structure"
  author:
  - name: "DeMeo, William"
    link: "https://researchr.org/alias/demeo%2C-william"
  year: "2021"
  doi: "10.48550/ARXIV.2103.09092"
  links:
    "url": "https://arxiv.org/abs/2103.09092"
  researchr: "https://researchr.org/publication/https%3A-doi.org-10.48550-arxiv.2103.09092"
  cites: 0
  citedby: 0
  kind: "misc"
  key: "https:-doi.org-10.48550-arxiv.2103.09092"
- 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: "Datatype-generic programming meets elaborator reflection"
  author:
  - name: "Hsiang-Shang Ko"
    link: "https://researchr.org/alias/hsiang-shang-ko"
  - name: "Liang-Ting Chen"
    link: "https://researchr.org/alias/liang-ting-chen"
  - name: "Tzu-Chi Lin"
    link: "https://researchr.org/alias/tzu-chi-lin"
  year: "2022"
  doi: "https://doi.org/10.1145/3547629"
  links:
    doi: "https://doi.org/10.1145/3547629"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/KoCL22"
  researchr: "https://researchr.org/publication/KoCL22-0"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "6"
  number: "ICFP"
  pages: "225-253"
  kind: "article"
  key: "KoCL22-0"
- title: "Algebra of Programming Using Dependent Types"
  author:
  - name: "Shin-Cheng Mu"
    link: "http://www.iis.sinica.edu.tw/~scm/"
  - name: "Hsiang-Shang Ko"
    link: "http://joshkos.blogspot.se/"
  - name: "Patrik Jansson"
    link: "http://www.chalmers.se/cse/EN/people/jansson-patrik"
  year: "2008"
  doi: "http://dx.doi.org/10.1007/978-3-540-70594-9_15"
  abstract: "Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. We demonstrate how to encode functional and relational derivations in a dependently typed programming language. A program is coupled with an algebraic derivation from a specification, whose correctness is guaranteed by the type system."
  links:
    doi: "http://dx.doi.org/10.1007/978-3-540-70594-9_15"
  tags:
  - "programming languages"
  - "functional programming"
  - "relational algebra"
  - "type system"
  - "algebraic specification"
  - " algebra"
  - "programming"
  - "type theory"
  researchr: "https://researchr.org/publication/MuKJ08"
  cites: 0
  citedby: 0
  pages: "268-283"
  booktitle: "mpc"
  kind: "inproceedings"
  key: "MuKJ08"
- title: "Certified normalization of generalized traces"
  author:
  - name: "Hendrik Maarand"
    link: "https://researchr.org/alias/hendrik-maarand"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  year: "2019"
  doi: "https://doi.org/10.1007/s11334-019-00347-1"
  links:
    doi: "https://doi.org/10.1007/s11334-019-00347-1"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/isse/MaarandU19"
  researchr: "https://researchr.org/publication/MaarandU19"
  cites: 0
  citedby: 0
  journal: "isse"
  volume: "15"
  number: "3-4"
  pages: "253-265"
  kind: "article"
  key: "MaarandU19"
- title: "Transporting functions across ornaments"
  author:
  - name: "Pierre-Évariste Dagand"
    link: "https://researchr.org/alias/pierre-%C3%A9variste-dagand"
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  year: "2014"
  doi: "http://dx.doi.org/10.1017/S0956796814000069"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796814000069"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/DagandM14"
  researchr: "https://researchr.org/publication/DagandM14"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "24"
  number: "2-3"
  pages: "316-383"
  kind: "article"
  key: "DagandM14"
- title: "A Constructive Model of Uniform Continuity"
  author:
  - name: "Chuangjie Xu"
    link: "https://researchr.org/alias/chuangjie-xu"
  - name: "Martín Hötzel Escardó"
    link: "https://researchr.org/alias/mart%C3%ADn-h%C3%B6tzel-escard%C3%B3"
  year: "2013"
  doi: "http://dx.doi.org/10.1007/978-3-642-38946-7_18"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-38946-7_18"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tlca/XuE13"
  researchr: "https://researchr.org/publication/XuE13-1"
  cites: 0
  citedby: 0
  pages: "236-249"
  booktitle: "tlca"
  kind: "inproceedings"
  key: "XuE13-1"
- title: "Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda"
  author:
  - name: "Harold Carr"
    link: "https://researchr.org/alias/harold-carr"
  - name: "Christa Jenkins"
    link: "https://researchr.org/alias/christa-jenkins"
  - name: "Mark Moir"
    link: "https://researchr.org/alias/mark-moir"
  - name: "Victor Cacciari Miraldo"
    link: "https://researchr.org/alias/victor-cacciari-miraldo"
  - name: "Lisandra Silva"
    link: "https://researchr.org/alias/lisandra-silva"
  year: "2022"
  doi: "https://doi.org/10.1007/978-3-031-06773-0_33"
  links:
    doi: "https://doi.org/10.1007/978-3-031-06773-0_33"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/nfm/CarrJMMS22"
  researchr: "https://researchr.org/publication/CarrJMMS22"
  cites: 0
  citedby: 0
  pages: "616-635"
  booktitle: "NFM"
  kind: "inproceedings"
  key: "CarrJMMS22"
- title: "Intrinsically typed compilation with nameless labels"
  author:
  - name: "Arjen Rouvoet"
    link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/"
  - name: "Robbert Krebbers"
    link: "https://researchr.org/alias/robbert-krebbers"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2021"
  doi: "https://doi.org/10.1145/3434303"
  abstract: "To avoid compilation errors it is desirable to verify that a compiler is type correct—i.e., given well-typed source code, it always outputs well-typed target code. This can be done intrinsically by implementing it as a function in a dependently typed programming language, such as Agda. This function manipulates data types of well-typed source and target programs, and is therefore type correct by construction. A key challenge in implementing an intrinsically typed compiler is the representation of labels in bytecode. Because label names are global, bytecode typing appears to be inherently a non-compositional, whole-program property. The individual operations of the compiler do not preserve this property, which requires the programmer to reason about labels, which spoils the compiler definition with proof terms. In this paper, we address this problem using a new nameless and co-contextual representation of typed global label binding, which is compositional. Our key idea is to use linearity to ensure that all labels are defined exactly once. To write concise compilers that manipulate programs in our representation, we develop a linear, dependently typed, shallowly embedded language in Agda, based on separation logic. We show that this language enables the concise specification and implementation of intrinsically typed operations on bytecode, culminating in an intrinsically typed compiler for a language with structured control-flow."
  links:
    doi: "https://doi.org/10.1145/3434303"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/RouvoetKV21"
  tags:
  - "Intrinsic-Verification"
  researchr: "https://researchr.org/publication/RouvoetKV21"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "5"
  number: "POPL"
  pages: "1-28"
  kind: "article"
  key: "RouvoetKV21"
- title: "Certified Normalization of Context-Free Grammars"
  author:
  - name: "Denis Firsov"
    link: "https://researchr.org/alias/denis-firsov"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  year: "2015"
  doi: "http://doi.acm.org/10.1145/2676724.2693177"
  links:
    doi: "http://doi.acm.org/10.1145/2676724.2693177"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/FirsovU15"
  researchr: "https://researchr.org/publication/FirsovU15"
  cites: 0
  citedby: 0
  pages: "167-174"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "FirsovU15"
- title: "The taming of the rew: a type theory with computational assumptions"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Nicolas Tabareau"
    link: "https://researchr.org/alias/nicolas-tabareau"
  - name: "Théo Winterhalter"
    link: "https://researchr.org/alias/th%C3%A9o-winterhalter"
  year: "2021"
  doi: "https://doi.org/10.1145/3434341"
  links:
    doi: "https://doi.org/10.1145/3434341"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/CockxTW21"
  researchr: "https://researchr.org/publication/CockxTW21"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "5"
  number: "POPL"
  pages: "1-29"
  kind: "article"
  key: "CockxTW21"
- title: "Constructive Galois Connections"
  author:
  - name: "David Darais"
    link: "https://researchr.org/alias/david-darais"
  - name: "David Van Horn"
    link: "https://researchr.org/alias/david-van-horn"
  year: "2019"
  doi: "https://doi.org/10.1017/S0956796819000066"
  links:
    doi: "https://doi.org/10.1017/S0956796819000066"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/DaraisH19"
  researchr: "https://researchr.org/publication/DaraisH19"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "29"
  kind: "article"
  key: "DaraisH19"
- title: "Dependently-Typed Formalisation of Relation-Algebraic Abstractions"
  author:
  - name: "Wolfram Kahl"
    link: "https://researchr.org/alias/wolfram-kahl"
  year: "2011"
  doi: "http://dx.doi.org/10.1007/978-3-642-21070-9_18"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-21070-9_18"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/RelMiCS/Kahl11"
  tags:
  - " algebra"
  - "abstraction"
  researchr: "https://researchr.org/publication/Kahl11-0"
  cites: 0
  citedby: 0
  pages: "230-247"
  booktitle: "RelMiCS"
  kind: "inproceedings"
  key: "Kahl11-0"
- title: "A cost-aware logical framework"
  author:
  - name: "Yue Niu"
    link: "https://researchr.org/alias/yue-niu"
  - name: "Jonathan Sterling"
    link: "https://researchr.org/alias/jonathan-sterling"
  - name: "Harrison Grodin"
    link: "https://researchr.org/alias/harrison-grodin"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2022"
  doi: "https://doi.org/10.1145/3498670"
  links:
    doi: "https://doi.org/10.1145/3498670"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/NiuSGH22"
  researchr: "https://researchr.org/publication/NiuSGH22"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "6"
  number: "POPL"
  pages: "1-31"
  kind: "article"
  key: "NiuSGH22"
- title: "Category theoretic structure of setoids"
  author:
  - name: "Yoshiki Kinoshita"
    link: "https://researchr.org/alias/yoshiki-kinoshita"
  - name: "John Power"
    link: "https://researchr.org/alias/john-power"
  year: "2014"
  doi: "http://dx.doi.org/10.1016/j.tcs.2014.03.006"
  links:
    doi: "http://dx.doi.org/10.1016/j.tcs.2014.03.006"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/tcs/KinoshitaP14"
  researchr: "https://researchr.org/publication/KinoshitaP14"
  cites: 0
  citedby: 0
  journal: "TCS"
  volume: "546"
  pages: "145-163"
  kind: "article"
  key: "KinoshitaP14"
- title: "Generic programming with indexed functors"
  author:
  - name: "Andres Löh"
    link: "https://researchr.org/alias/andres-l%C3%B6h"
  - name: "José Pedro Magalhães"
    link: "https://researchr.org/alias/jos%C3%A9-pedro-magalh%C3%A3es"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/2036918.2036920"
  links:
    doi: "http://doi.acm.org/10.1145/2036918.2036920"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/LohM11"
  researchr: "https://researchr.org/publication/LohM11"
  cites: 0
  citedby: 0
  pages: "1-12"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "LohM11"
- title: "Correct-by-construction pretty-printing"
  author:
  - name: "Nils Anders Danielsson"
    link: "https://researchr.org/alias/nils-anders-danielsson"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2502409.2502410"
  links:
    doi: "http://doi.acm.org/10.1145/2502409.2502410"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/Danielsson13"
  researchr: "https://researchr.org/publication/Danielsson13"
  cites: 0
  citedby: 0
  pages: "1-12"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "Danielsson13"
- title: "More dependent types for distributed arrays"
  author:
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/s10990-011-9075-y"
  links:
    doi: "http://dx.doi.org/10.1007/s10990-011-9075-y"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/lisp/Swierstra10"
  researchr: "https://researchr.org/publication/Swierstra10"
  cites: 0
  citedby: 0
  journal: "lisp"
  volume: "23"
  number: "4"
  pages: "489-506"
  kind: "article"
  key: "Swierstra10"
- title: "Djinn, Monotonic"
  author:
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  year: "2010"
  doi: "http://www.easychair.org/publications/?page=711183398"
  links:
    doi: "http://www.easychair.org/publications/?page=711183398"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/McBride10"
  researchr: "https://researchr.org/publication/McBride10-2"
  cites: 0
  citedby: 0
  pages: "14-17"
  booktitle: "itp"
  kind: "inproceedings"
  key: "McBride10-2"
- title: "π with Leftovers: A Mechanisation in Agda"
  author:
  - name: "Uma Zalakain"
    link: "https://researchr.org/alias/uma-zalakain"
  - name: "Ornela Dardha"
    link: "https://researchr.org/alias/ornela-dardha"
  year: "2021"
  doi: "https://doi.org/10.1007/978-3-030-78089-0_9"
  links:
    doi: "https://doi.org/10.1007/978-3-030-78089-0_9"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/forte/ZalakainD21"
  researchr: "https://researchr.org/publication/ZalakainD21"
  cites: 0
  citedby: 0
  pages: "157-174"
  booktitle: "forte"
  kind: "inproceedings"
  key: "ZalakainD21"
- title: "Observational equality: now for good"
  author:
  - name: "Loïc Pujet"
    link: "https://researchr.org/alias/lo%C3%AFc-pujet"
  - name: "Nicolas Tabareau"
    link: "https://researchr.org/alias/nicolas-tabareau"
  year: "2022"
  doi: "https://doi.org/10.1145/3498693"
  links:
    doi: "https://doi.org/10.1145/3498693"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/PujetT22"
  researchr: "https://researchr.org/publication/PujetT22"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "6"
  number: "POPL"
  pages: "1-27"
  kind: "article"
  key: "PujetT22"
- title: "Security-typed programming within dependently typed programming"
  author:
  - name: "Jamie Morgenstern"
    link: "https://researchr.org/alias/jamie-morgenstern"
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863543.1863569"
  links:
    doi: "http://doi.acm.org/10.1145/1863543.1863569"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/MorgensternL10"
  tags:
  - "security"
  - "programming"
  researchr: "https://researchr.org/publication/MorgensternL10"
  cites: 0
  citedby: 0
  pages: "169-180"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "MorgensternL10"
- title: "Programming interfaces and basic topology"
  author:
  - name: "Peter Hancock"
    link: "https://researchr.org/alias/peter-hancock"
  - name: "Pierre Hyvernat"
    link: "https://researchr.org/alias/pierre-hyvernat"
  year: "2006"
  doi: "http://dx.doi.org/10.1016/j.apal.2005.05.022"
  links:
    doi: "http://dx.doi.org/10.1016/j.apal.2005.05.022"
  tags:
  - "programming"
  researchr: "https://researchr.org/publication/HancockH06"
  cites: 0
  citedby: 0
  journal: "APAL"
  volume: "137"
  number: "1-3"
  pages: "189-239"
  kind: "article"
  key: "HancockH06"
- title: "Calculating dependently-typed compilers (functional pearl)"
  author:
  - name: "Mitchell Pickard"
    link: "https://researchr.org/alias/mitchell-pickard"
  - name: "Graham Hutton"
    link: "https://researchr.org/alias/graham-hutton"
  year: "2021"
  doi: "https://doi.org/10.1145/3473587"
  links:
    doi: "https://doi.org/10.1145/3473587"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/PickardH21"
  researchr: "https://researchr.org/publication/PickardH21"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "5"
  number: "ICFP"
  pages: "1-27"
  kind: "article"
  key: "PickardH21"
- title: "Typed syntactic meta-programming"
  author:
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2500365.2500575"
  links:
    doi: "http://doi.acm.org/10.1145/2500365.2500575"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/DevrieseP13"
  researchr: "https://researchr.org/publication/DevrieseP13"
  cites: 0
  citedby: 0
  pages: "73-86"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "DevrieseP13"
- title: "Timely Computation"
  author:
  - name: "Conal Elliott"
    link: "https://researchr.org/alias/conal-elliott"
  year: "2023"
  month: "August"
  doi: "https://doi.org/10.1145/3607861"
  links:
    doi: "https://doi.org/10.1145/3607861"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/Elliott23"
  researchr: "https://researchr.org/publication/Elliott23-0"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "7"
  number: "ICFP"
  pages: "895-919"
  kind: "article"
  key: "Elliott23-0"
- title: "Intrinsically-typed definitional interpreters for imperative languages"
  author:
  - name: "Casper Bach Poulsen"
    link: "http://www.casperbp.net"
  - name: "Arjen Rouvoet"
    link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Robbert Krebbers"
    link: "https://robbertkrebbers.nl"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2018"
  doi: "http://doi.acm.org/10.1145/3158104"
  abstract: " A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a separate type system requires a separate type safety proof. An alternative approach, at least for pure object languages, is to use a dependently-typed language to encode the object language type system in the definition of the abstract syntax. Using such intrinsically-typed abstract syntax definitions allows the host language type checker to verify automatically that the interpreter satisfies type safety. Does this approach scale to larger and more realistic object languages, and in particular to languages with mutable state and objects? In this paper, we describe and demonstrate techniques and libraries in Agda that successfully scale up intrinsically-typed definitional interpreters to handle rich object languages with non-trivial binding structures and mutable state. While the resulting interpreters are certainly more complex than the simply-typed λ-calculus interpreter we start with, we claim that they still meet the goals of being concise, comprehensible, and executable, while guaranteeing type safety for more elaborate object languages. We make the following contributions: (1) A dependent-passing style technique for hiding the weakening of indexed values as they propagate through monadic code. (2) An Agda library for programming with scope graphs and frames, which provides a uniform approach to dealing with name binding in intrinsically-typed interpreters. (3) Case studies of intrinsically-typed definitional interpreters for the simply-typed λ-calculus with references (STLC+Ref) and for a large subset of Middleweight Java (MJ). "
  links:
    doi: "http://doi.acm.org/10.1145/3158104"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/PoulsenRTKV18"
    technicalreport: "https://researchr.org/publication/preprint-PoulsenRTKV18"
  tags:
  - "Intrinsic-Verification"
  researchr: "https://researchr.org/publication/PoulsenRTKV18"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "2"
  number: "POPL"
  kind: "article"
  key: "PoulsenRTKV18"
- 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: "Integrating an Automated Theorem Prover into Agda"
  author:
  - name: "Simon Foster"
    link: "https://researchr.org/alias/simon-foster"
  - name: "Georg Struth"
    link: "https://researchr.org/alias/georg-struth"
  year: "2011"
  doi: "http://dx.doi.org/10.1007/978-3-642-20398-5_10"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-20398-5_10"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/nfm/FosterS11"
  researchr: "https://researchr.org/publication/FosterS11-0"
  cites: 0
  citedby: 0
  pages: "116-130"
  booktitle: "NFM"
  kind: "inproceedings"
  key: "FosterS11-0"
- title: "Pi-Ware: Hardware Description and Verification in Agda"
  author:
  - name: "João Paulo Pizani Flor"
    link: "https://researchr.org/alias/jo%C3%A3o-paulo-pizani-flor"
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  - name: "Yorick Sijsling"
    link: "https://researchr.org/alias/yorick-sijsling"
  year: "2015"
  doi: "https://doi.org/10.4230/LIPIcs.TYPES.2015.9"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.TYPES.2015.9"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/types/FlorSS15"
  tags:
  - "Intrinsic-Verification"
  researchr: "https://researchr.org/publication/FlorSS15"
  cites: 0
  citedby: 0
  booktitle: "TYPES"
  kind: "inproceedings"
  key: "FlorSS15"
- title: "Dependent Pattern Matching and Proof-Relevant Unification"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  year: "2017"
  doi: "https://www.base-search.net/Record/66a7ce9719c00dd2b976ac2c0f472c9fa527c0fcc5fbe259b2c5ca71b4f5ecc7"
  links:
    doi: "https://www.base-search.net/Record/66a7ce9719c00dd2b976ac2c0f472c9fa527c0fcc5fbe259b2c5ca71b4f5ecc7"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/basesearch/Cockx17"
  researchr: "https://researchr.org/publication/basesearch-7836"
  cites: 0
  citedby: 0
  school: "Katholieke Universiteit Leuven, Belgium"
  kind: "phdthesis"
  key: "basesearch-7836"
- title: "On homotopy of walks and spherical maps in homotopy type theory"
  author:
  - name: "Jonathan Prieto-Cubides"
    link: "https://researchr.org/alias/jonathan-prieto-cubides"
  year: "2022"
  doi: "https://doi.org/10.1145/3497775.3503671"
  links:
    doi: "https://doi.org/10.1145/3497775.3503671"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/Prieto-Cubides22"
  researchr: "https://researchr.org/publication/Prieto-Cubides22"
  cites: 0
  citedby: 0
  pages: "338-351"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "Prieto-Cubides22"
- title: "Termination Checking in the Presence of Nested Inductive and Coinductive Types"
  author:
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  - name: "Nils Anders Danielsson"
    link: "https://researchr.org/alias/nils-anders-danielsson"
  year: "2010"
  doi: "http://www.easychair.org/publications/?page=751599912"
  links:
    doi: "http://www.easychair.org/publications/?page=751599912"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/AltenkirchD10"
  researchr: "https://researchr.org/publication/AltenkirchD10"
  cites: 0
  citedby: 0
  pages: "100-105"
  booktitle: "itp"
  kind: "inproceedings"
  key: "AltenkirchD10"
- title: "Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer Lemma"
  author:
  - name: "Hannes Saffrich"
    link: "https://researchr.org/alias/hannes-saffrich"
  - name: "Peter Thiemann 0001"
    link: "https://researchr.org/alias/peter-thiemann-0001"
  - name: "Marius Weidner"
    link: "https://researchr.org/alias/marius-weidner"
  year: "2024"
  doi: "https://doi.org/10.1145/3678000.3678201"
  links:
    doi: "https://doi.org/10.1145/3678000.3678201"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tyde/Saffrich0W24"
  researchr: "https://researchr.org/publication/Saffrich0W24"
  cites: 0
  citedby: 0
  pages: "2-15"
  booktitle: "tyde"
  kind: "inproceedings"
  key: "Saffrich0W24"
- title: "Internal and Observational Parametricity for Cubical Agda"
  author:
  - name: "Antoine Van Muylder"
    link: "https://researchr.org/alias/antoine-van-muylder"
  - name: "Andreas Nuyts"
    link: "https://researchr.org/alias/andreas-nuyts"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2024"
  month: "January"
  doi: "https://doi.org/10.1145/3632850"
  links:
    doi: "https://doi.org/10.1145/3632850"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/MuylderND24"
  researchr: "https://researchr.org/publication/MuylderND24"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "8"
  number: "POPL"
  pages: "209-240"
  kind: "article"
  key: "MuylderND24"
- title: "The Functor of Points Approach to Schemes in Cubical Agda"
  author:
  - name: "Max Zeuner"
    link: "https://researchr.org/alias/max-zeuner"
  - name: "Matthias Hutzler"
    link: "https://researchr.org/alias/matthias-hutzler"
  year: "2024"
  doi: "https://doi.org/10.4230/LIPIcs.ITP.2024.38"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.ITP.2024.38"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/ZeunerH24"
  researchr: "https://researchr.org/publication/ZeunerH24"
  cites: 0
  citedby: 0
  booktitle: "itp"
  kind: "inproceedings"
  key: "ZeunerH24"
- title: "Computing with Semirings and Weak Rig Groupoids"
  author:
  - name: "Jacques Carette"
    link: "https://researchr.org/alias/jacques-carette"
  - name: "Amr Sabry"
    link: "https://researchr.org/alias/amr-sabry"
  year: "2016"
  doi: "http://dx.doi.org/10.1007/978-3-662-49498-1_6"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-662-49498-1_6"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/CaretteS16"
  researchr: "https://researchr.org/publication/CaretteS16-0"
  cites: 0
  citedby: 0
  pages: "123-148"
  booktitle: "ESOP"
  kind: "inproceedings"
  key: "CaretteS16-0"
- title: "Extracting the power of dependent types"
  author:
  - name: "Artjoms Sinkarovs"
    link: "https://researchr.org/alias/artjoms-sinkarovs"
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  year: "2021"
  doi: "https://doi.org/10.1145/3486609.3487201"
  links:
    doi: "https://doi.org/10.1145/3486609.3487201"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/gpce/SinkarovsC21"
  researchr: "https://researchr.org/publication/SinkarovsC21"
  cites: 0
  citedby: 0
  pages: "83-95"
  booktitle: "GPCE"
  kind: "inproceedings"
  key: "SinkarovsC21"
- title: "Small Induction Recursion"
  author:
  - name: "Peter Hancock"
    link: "https://researchr.org/alias/peter-hancock"
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  - name: "Neil Ghani"
    link: "https://researchr.org/alias/neil-ghani"
  - name: "Lorenzo Malatesta"
    link: "https://researchr.org/alias/lorenzo-malatesta"
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  year: "2013"
  doi: "http://dx.doi.org/10.1007/978-3-642-38946-7_13"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-38946-7_13"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tlca/HancockMGMA13"
  researchr: "https://researchr.org/publication/HancockMGMA13"
  cites: 0
  citedby: 0
  pages: "156-172"
  booktitle: "tlca"
  kind: "inproceedings"
  key: "HancockMGMA13"
- title: "Lifting proof-relevant unification to higher dimensions"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3018610.3018612"
  links:
    doi: "http://doi.acm.org/10.1145/3018610.3018612"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/CockxD17"
  researchr: "https://researchr.org/publication/CockxD17"
  cites: 0
  citedby: 0
  pages: "173-181"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "CockxD17"
- title: "Formal derivation of Greedy algorithms from relational specifications: A tutorial"
  author:
  - name: "Yu-Hsi Chiang"
    link: "https://researchr.org/alias/yu-hsi-chiang"
  - name: "Shin-Cheng Mu"
    link: "https://researchr.org/alias/shin-cheng-mu"
  year: "2016"
  doi: "http://dx.doi.org/10.1016/j.jlamp.2015.12.003"
  links:
    doi: "http://dx.doi.org/10.1016/j.jlamp.2015.12.003"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jlp/ChiangM16"
  researchr: "https://researchr.org/publication/ChiangM16"
  cites: 0
  citedby: 0
  journal: "jlp"
  volume: "85"
  number: "5"
  pages: "879-905"
  kind: "article"
  key: "ChiangM16"
- title: "Eliminating dependent pattern matching without K"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  year: "2016"
  doi: "http://dx.doi.org/10.1017/S0956796816000174"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796816000174"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/CockxDP16"
  researchr: "https://researchr.org/publication/CockxDP16-0"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "26"
  kind: "article"
  key: "CockxDP16-0"
- title: "Type-safe diff for families of datatypes"
  author:
  - name: "Eelco Lempsink"
    link: "http://eelco.lempsink.nl/"
  - name: "Sean Leather"
    link: "http://www.cs.uu.nl/staff/leather.html"
  - name: "Andres Löh"
    link: "http://people.cs.uu.nl/andres/"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1596614.1596624"
  abstract: "The UNIX diff program finds the difference between two text files using a classic algorithm for determining the longest common subsequence; however, when working with structured input (e.g. program code), we often want to find the difference between tree-like data (e.g. the abstract syntax tree). In a functional programming language such as Haskell, we can represent this data with a family of (mutually recursive) datatypes. In this paper, we describe a functional, datatype-generic implementation of diff (and the associated program patch). Our approach requires advanced type system features to preserve type safety; therefore, we present the code in Agda, a dependently-typed language well-suited to datatype-generic programming. In order to establish the usefulness of our work, we show that its efficiency can be improved with memoization and that it can also be defined in Haskell. "
  links:
    doi: "http://doi.acm.org/10.1145/1596614.1596624"
  tags:
  - "programming languages"
  - "data-flow language"
  - "generic programming"
  - "abstract syntax"
  - "functional programming"
  - "Haskell"
  - "type system"
  - "data-flow programming"
  - "data-flow"
  - "programming"
  - "systematic-approach"
  researchr: "https://researchr.org/publication/LLL09diff"
  cites: 0
  citedby: 0
  booktitle: "WGP '09: Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming"
  kind: "inproceedings"
  key: "LLL09diff"
- title: "From algebra to abstract machine: a verified generic construction"
  author:
  - name: "Carlos Tomé Cortiñas"
    link: "https://researchr.org/alias/carlos-tom%C3%A9-corti%C3%B1as"
  - name: "Wouter Swierstra"
    link: "https://researchr.org/alias/wouter-swierstra"
  year: "2018"
  doi: "https://doi.org/10.1145/3240719.3241787"
  links:
    doi: "https://doi.org/10.1145/3240719.3241787"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/CortinasS18"
  researchr: "https://researchr.org/publication/CortinasS18"
  cites: 0
  citedby: 0
  pages: "78-90"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "CortinasS18"
- title: "Krivine nets: a semantic foundation for distributed execution"
  author:
  - name: "Olle Fredriksson"
    link: "https://researchr.org/alias/olle-fredriksson"
  - name: "Dan R. Ghica"
    link: "http://www.cs.bham.ac.uk/~drg/"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2628136.2628152"
  links:
    doi: "http://doi.acm.org/10.1145/2628136.2628152"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/FredrikssonG14"
  researchr: "https://researchr.org/publication/FredrikssonG14-0"
  cites: 0
  citedby: 0
  pages: "349-361"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "FredrikssonG14-0"
- title: "Cubical agda: a dependently typed programming language with univalence and higher inductive types"
  author:
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  - name: "Anders Mörtberg"
    link: "https://researchr.org/alias/anders-m%C3%B6rtberg"
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  year: "2019"
  doi: "https://doi.org/10.1145/3341691"
  links:
    doi: "https://doi.org/10.1145/3341691"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/VezzosiM019"
  researchr: "https://researchr.org/publication/VezzosiM019"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "3"
  number: "ICFP"
  kind: "article"
  key: "VezzosiM019"
- title: "Continuity of Gödel's System T Definable Functionals via Effectful Forcing"
  author:
  - name: "Martín Hötzel Escardó"
    link: "https://researchr.org/alias/mart%C3%ADn-h%C3%B6tzel-escard%C3%B3"
  year: "2013"
  doi: "http://dx.doi.org/10.1016/j.entcs.2013.09.010"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2013.09.010"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/entcs/Escardo13"
  researchr: "https://researchr.org/publication/Escardo13-0"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "298"
  pages: "119-141"
  kind: "article"
  key: "Escardo13-0"
- title: "Certified CYK parsing of context-free languages"
  author:
  - name: "Denis Firsov"
    link: "https://researchr.org/alias/denis-firsov"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  year: "2014"
  doi: "http://dx.doi.org/10.1016/j.jlamp.2014.09.002"
  links:
    doi: "http://dx.doi.org/10.1016/j.jlamp.2014.09.002"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jlp/FirsovU14"
  researchr: "https://researchr.org/publication/FirsovU14"
  cites: 0
  citedby: 0
  journal: "jlp"
  volume: "83"
  number: "5-6"
  pages: "459-468"
  kind: "article"
  key: "FirsovU14"
- title: "Formalizing Constructive Projective Geometry in Agda"
  author:
  - name: "Guillermo Calderón"
    link: "https://researchr.org/alias/guillermo-calder%C3%B3n"
  year: "2018"
  doi: "https://doi.org/10.1016/j.entcs.2018.10.005"
  links:
    doi: "https://doi.org/10.1016/j.entcs.2018.10.005"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/entcs/Calderon18"
  researchr: "https://researchr.org/publication/Calderon18"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "338"
  pages: "61-77"
  kind: "article"
  key: "Calderon18"
- title: "Constructive Analysis in the Agda Proof Assistant"
  author:
  - name: "Murray, Zachary"
    link: "https://researchr.org/alias/murray%2C-zachary"
  year: "2022"
  doi: "10.48550/ARXIV.2205.08354"
  links:
    "url": "https://arxiv.org/abs/2205.08354"
  researchr: "https://researchr.org/publication/https%3A-doi.org-10.48550-arxiv.2205.08354"
  cites: 0
  citedby: 0
  kind: "misc"
  key: "https:-doi.org-10.48550-arxiv.2205.08354"
- title: "A simulator of Solidity-style smart contracts in the theorem prover Agda"
  author:
  - name: "Fahad F. Alhabardi"
    link: "https://researchr.org/alias/fahad-f.-alhabardi"
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  year: "2023"
  doi: "https://doi.org/10.1145/3651655.3651656"
  links:
    doi: "https://doi.org/10.1145/3651655.3651656"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icbta/AlhabardiS23"
  researchr: "https://researchr.org/publication/AlhabardiS23-0"
  cites: 0
  citedby: 0
  pages: "1-11"
  booktitle: "icbta"
  kind: "inproceedings"
  key: "AlhabardiS23-0"
- title: "Cubical Agda: A dependently typed programming language with univalence and higher inductive types"
  author:
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  - name: "Anders Mörtberg"
    link: "https://researchr.org/alias/anders-m%C3%B6rtberg"
  - name: "Andreas Abel 0001"
    link: "https://researchr.org/alias/andreas-abel-0001"
  year: "2021"
  doi: "https://doi.org/10.1017/S0956796821000034"
  links:
    doi: "https://doi.org/10.1017/S0956796821000034"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/VezzosiMA21"
  researchr: "https://researchr.org/publication/VezzosiMA21"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "31"
  kind: "article"
  key: "VezzosiMA21"
- title: "Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs"
  author:
  - name: "Ana Bove"
    link: "https://researchr.org/alias/ana-bove"
  - name: "Peter Dybjer"
    link: "https://researchr.org/alias/peter-dybjer"
  - name: "Andrés Sicard-Ramírez"
    link: "https://researchr.org/alias/andr%C3%A9s-sicard-ram%C3%ADrez"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/978-3-642-28729-9_7"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-28729-9_7"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fossacs/BoveDS12"
  researchr: "https://researchr.org/publication/BoveDS12"
  cites: 0
  citedby: 0
  pages: "104-118"
  booktitle: "fossacs"
  kind: "inproceedings"
  key: "BoveDS12"
- title: "Causality for free!: parametricity implies causality for functional reactive programs"
  author:
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2428116.2428127"
  links:
    doi: "http://doi.acm.org/10.1145/2428116.2428127"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/plpv/Jeffrey13"
  researchr: "https://researchr.org/publication/Jeffrey13-0"
  cites: 0
  citedby: 0
  pages: "57-68"
  booktitle: "plpv"
  kind: "inproceedings"
  key: "Jeffrey13-0"
- title: "Synthetic Integral Cohomology in Cubical Agda"
  author:
  - name: "Guillaume Brunerie"
    link: "https://researchr.org/alias/guillaume-brunerie"
  - name: "Axel Ljungström"
    link: "https://researchr.org/alias/axel-ljungstr%C3%B6m"
  - name: "Anders Mörtberg"
    link: "https://researchr.org/alias/anders-m%C3%B6rtberg"
  year: "2022"
  doi: "https://doi.org/10.4230/LIPIcs.CSL.2022.11"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.CSL.2022.11"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/BrunerieLM22"
  researchr: "https://researchr.org/publication/BrunerieLM22"
  cites: 0
  citedby: 0
  booktitle: "csl"
  kind: "inproceedings"
  key: "BrunerieLM22"
- title: "Encoding Agda Programs Using Rewriting"
  author:
  - name: "Guillaume Genestier"
    link: "https://researchr.org/alias/guillaume-genestier"
  year: "2020"
  doi: "https://doi.org/10.4230/LIPIcs.FSCD.2020.31"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.FSCD.2020.31"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fscd/Genestier20"
  researchr: "https://researchr.org/publication/Genestier20"
  cites: 0
  citedby: 0
  booktitle: "fscd"
  kind: "inproceedings"
  key: "Genestier20"
- title: "A unified treatment of syntax with binders"
  author:
  - name: "Nicolas Pouillard"
    link: "https://researchr.org/alias/nicolas-pouillard"
  - name: "François Pottier"
    link: "https://researchr.org/alias/fran%C3%A7ois-pottier"
  year: "2012"
  doi: "http://dx.doi.org/10.1017/S0956796812000251"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796812000251"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/PouillardP12"
  researchr: "https://researchr.org/publication/PouillardP12"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "22"
  number: "4-5"
  pages: "614-704"
  kind: "article"
  key: "PouillardP12"
- title: "Homotopical patch theory"
  author:
  - name: "Carlo Angiuli"
    link: "https://researchr.org/alias/carlo-angiuli"
  - name: "Edward Morehouse"
    link: "https://researchr.org/alias/edward-morehouse"
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2628136.2628158"
  links:
    doi: "http://doi.acm.org/10.1145/2628136.2628158"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/AngiuliMLH14"
  researchr: "https://researchr.org/publication/AngiuliMLH14"
  cites: 0
  citedby: 0
  pages: "243-256"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "AngiuliMLH14"
- title: "Formalizing π-calculus in guarded cubical Agda"
  author:
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  year: "2020"
  doi: "https://doi.org/10.1145/3372885.3373814"
  links:
    doi: "https://doi.org/10.1145/3372885.3373814"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/VeltriV20"
  researchr: "https://researchr.org/publication/VeltriV20"
  cites: 0
  citedby: 0
  pages: "270-283"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "VeltriV20"
- title: "Finiteness and rational sequences, constructively"
  author:
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  year: "2017"
  doi: "http://dx.doi.org/10.1017/S0956796817000041"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796817000041"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/UustaluV17"
  researchr: "https://researchr.org/publication/UustaluV17"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "27"
  kind: "article"
  key: "UustaluV17"
- title: "Leveling up dependent types: generic programming over a predicative hierarchy of universes"
  author:
  - name: "Larry Diehl"
    link: "https://researchr.org/alias/larry-diehl"
  - name: "Tim Sheard"
    link: "https://researchr.org/alias/tim-sheard"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2502409.2502414"
  links:
    doi: "http://doi.acm.org/10.1145/2502409.2502414"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/DiehlS13"
  researchr: "https://researchr.org/publication/DiehlS13"
  cites: 0
  citedby: 0
  pages: "49-60"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "DiehlS13"
- title: "Live functional programming with typed holes"
  author:
  - name: "Cyrus Omar"
    link: "https://researchr.org/alias/cyrus-omar"
  - name: "Ian Voysey"
    link: "https://researchr.org/alias/ian-voysey"
  - name: "Ravi Chugh"
    link: "https://researchr.org/alias/ravi-chugh"
  - name: "Matthew A. Hammer"
    link: "https://researchr.org/alias/matthew-a.-hammer"
  year: "2019"
  doi: "https://dl.acm.org/citation.cfm?id=3290327"
  links:
    doi: "https://dl.acm.org/citation.cfm?id=3290327"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/OmarVCH19"
  researchr: "https://researchr.org/publication/OmarVCH19"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "3"
  kind: "article"
  key: "OmarVCH19"
- title: "A universe of binding and computation"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1596550.1596571"
  links:
    doi: "http://doi.acm.org/10.1145/1596550.1596571"
  researchr: "https://researchr.org/publication/LicataH09"
  cites: 0
  citedby: 0
  pages: "123-134"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "LicataH09"
- title: "A model of Solidity-style smart contracts in the theorem prover Agda"
  author:
  - name: "Fahad F. Alhabardi"
    link: "https://researchr.org/alias/fahad-f.-alhabardi"
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  year: "2023"
  doi: "https://doi.org/10.1109/AIBThings58340.2023.10292478"
  links:
    doi: "https://doi.org/10.1109/AIBThings58340.2023.10292478"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/aibthings/AlhabardiS23"
  researchr: "https://researchr.org/publication/AlhabardiS23"
  cites: 0
  citedby: 0
  pages: "1-10"
  booktitle: "aibthings"
  kind: "inproceedings"
  key: "AlhabardiS23"
- title: "Formalizing Restriction Categories"
  author:
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  year: "2017"
  doi: "https://doi.org/10.6092/issn.1972-5787/6237"
  links:
    doi: "https://doi.org/10.6092/issn.1972-5787/6237"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfrea/ChapmanUV17"
  researchr: "https://researchr.org/publication/ChapmanUV17"
  cites: 0
  citedby: 0
  journal: "jfrea"
  volume: "10"
  number: "1"
  pages: "1-36"
  kind: "article"
  key: "ChapmanUV17"
- title: "Formalizing Affinization of a Projective Plane in Agda"
  author:
  - name: "Calderón, Guillermo"
    link: "https://researchr.org/alias/calder%C3%B3n%2C-guillermo"
  year: "2021"
  doi: "10.1109/CLEI53233.2021.9640056"
  researchr: "https://researchr.org/publication/9640056"
  cites: 0
  citedby: 0
  pages: "1-8"
  booktitle: "2021 XLVII Latin American Computing Conference (CLEI)"
  kind: "inproceedings"
  key: "9640056"
- title: "Hereditary Substitutions for Simple Types, Formalized"
  author:
  - name: "Chantal Keller"
    link: "https://researchr.org/alias/chantal-keller"
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863597.1863601"
  links:
    doi: "http://doi.acm.org/10.1145/1863597.1863601"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/KellerA10"
  researchr: "https://researchr.org/publication/KellerA10"
  cites: 0
  citedby: 0
  pages: "3-10"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "KellerA10"
- title: "Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda"
  author:
  - name: "Ernesto Copello"
    link: "https://researchr.org/alias/ernesto-copello"
  - name: "Alvaro Tasistro"
    link: "https://researchr.org/alias/alvaro-tasistro"
  - name: "Bruno Bianchi"
    link: "https://researchr.org/alias/bruno-bianchi"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-319-11863-5_5"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-11863-5_5"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sblp/CopelloTB14"
  researchr: "https://researchr.org/publication/CopelloTB14"
  cites: 0
  citedby: 0
  pages: "62-76"
  booktitle: "SBLP"
  kind: "inproceedings"
  key: "CopelloTB14"
- title: "Inductive-Inductive Definitions"
  author:
  - name: "Fredrik Nordvall Forsberg"
    link: "https://researchr.org/alias/fredrik-nordvall-forsberg"
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/978-3-642-15205-4_35"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-15205-4_35"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/ForsbergS10"
  researchr: "https://researchr.org/publication/ForsbergS10"
  cites: 0
  citedby: 0
  pages: "454-468"
  booktitle: "csl"
  kind: "inproceedings"
  key: "ForsbergS10"
- title: "Specification and Verification of a Linear-Time Temporal Logic for Graph Transformation"
  author:
  - name: "Fabio Gadducci"
    link: "https://researchr.org/alias/fabio-gadducci"
  - name: "Andrea Laretto"
    link: "https://researchr.org/alias/andrea-laretto"
  - name: "Davide Trotta"
    link: "https://researchr.org/alias/davide-trotta"
  year: "2023"
  doi: "https://doi.org/10.1007/978-3-031-36709-0_2"
  links:
    doi: "https://doi.org/10.1007/978-3-031-36709-0_2"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/gg/GadducciLT23"
  researchr: "https://researchr.org/publication/GadducciLT23"
  cites: 0
  citedby: 0
  pages: "22-42"
  booktitle: "gg"
  kind: "inproceedings"
  key: "GadducciLT23"
- title: "Programming Language Foundations in Agda"
  author:
  - name: "Philip Wadler"
    link: "https://researchr.org/alias/philip-wadler"
  year: "2018"
  doi: "https://doi.org/10.1007/978-3-030-03044-5_5"
  links:
    doi: "https://doi.org/10.1007/978-3-030-03044-5_5"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sbmf/Wadler18"
  researchr: "https://researchr.org/publication/Wadler18"
  cites: 0
  citedby: 0
  pages: "56-73"
  booktitle: "sbmf"
  kind: "inproceedings"
  key: "Wadler18"
- title: "Expressive and strongly type-safe code generation"
  author:
  - name: "Thomas Winant"
    link: "https://researchr.org/alias/thomas-winant"
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3131851.3131872"
  links:
    doi: "http://doi.acm.org/10.1145/3131851.3131872"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/WinantCD17"
  researchr: "https://researchr.org/publication/WinantCD17"
  cites: 0
  citedby: 0
  pages: "199-210"
  booktitle: "ppdp"
  kind: "inproceedings"
  key: "WinantCD17"
- title: "Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda Calculus"
  author:
  - name: "Alvaro Tasistro"
    link: "https://researchr.org/alias/alvaro-tasistro"
  - name: "Ernesto Copello"
    link: "https://researchr.org/alias/ernesto-copello"
  - name: "Nora Szasz"
    link: "https://researchr.org/alias/nora-szasz"
  year: "2015"
  doi: "http://dx.doi.org/10.1016/j.entcs.2015.04.013"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2015.04.013"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/entcs/TasistroCS15"
  researchr: "https://researchr.org/publication/TasistroCS15"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "312"
  pages: "215-230"
  kind: "article"
  key: "TasistroCS15"
- title: "Normalization by evaluation for sized dependent types"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  - name: "Théo Winterhalter"
    link: "https://researchr.org/alias/th%C3%A9o-winterhalter"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3110277"
  links:
    doi: "http://doi.acm.org/10.1145/3110277"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/0001VW17"
  researchr: "https://researchr.org/publication/0001VW17"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "1"
  number: "ICFP"
  kind: "article"
  key: "0001VW17"
- title: "A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation"
  author:
  - name: "Yufei Cai"
    link: "https://researchr.org/alias/yufei-cai"
  - name: "Paolo G. Giarrusso"
    link: "https://www.informatik.uni-marburg.de/~pgiarrusso/"
  - name: "Tillmann Rendel"
    link: "https://researchr.org/alias/tillmann-rendel"
  - name: "Klaus Ostermann"
    link: "https://researchr.org/alias/klaus-ostermann"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2594291.2594304"
  links:
    doi: "http://doi.acm.org/10.1145/2594291.2594304"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pldi/CaiGRO14"
  researchr: "https://researchr.org/publication/CaiGRO14"
  cites: 0
  citedby: 0
  pages: "17"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "CaiGRO14"
- title: "Generalizations of Hedberg's Theorem"
  author:
  - name: "Nicolai Kraus"
    link: "https://researchr.org/alias/nicolai-kraus"
  - name: "Martín Hötzel Escardó"
    link: "https://researchr.org/alias/mart%C3%ADn-h%C3%B6tzel-escard%C3%B3"
  - name: "Thierry Coquand"
    link: "https://researchr.org/alias/thierry-coquand"
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  year: "2013"
  doi: "http://dx.doi.org/10.1007/978-3-642-38946-7_14"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-38946-7_14"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tlca/KrausECA13"
  researchr: "https://researchr.org/publication/KrausECA13"
  cites: 0
  citedby: 0
  pages: "173-188"
  booktitle: "tlca"
  kind: "inproceedings"
  key: "KrausECA13"
- title: "Truncation levels in homotopy type theory"
  author:
  - name: "Nicolai Kraus"
    link: "https://researchr.org/alias/nicolai-kraus"
  year: "2015"
  doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.668635"
  links:
    doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.668635"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/ethos/Kraus15"
  researchr: "https://researchr.org/publication/ethos-10479"
  cites: 0
  citedby: 0
  school: "University of Nottingham, UK"
  kind: "phdthesis"
  key: "ethos-10479"
- title: "A Machine-Checked Proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory"
  author:
  - name: "William J. DeMeo"
    link: "https://researchr.org/alias/william-j.-demeo"
  - name: "Jacques Carette"
    link: "https://researchr.org/alias/jacques-carette"
  year: "2021"
  doi: "https://doi.org/10.4230/LIPIcs.TYPES.2021.4"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.TYPES.2021.4"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/types/DeMeoC21"
  researchr: "https://researchr.org/publication/DeMeoC21"
  cites: 0
  citedby: 0
  booktitle: "TYPES"
  kind: "inproceedings"
  key: "DeMeoC21"
- title: "Observational equality, now!"
  author:
  - name: "Thorsten Altenkirch"
    link: "http://www.cs.nott.ac.uk/~txa"
  - name: "Conor McBride"
    link: "http://personal.cis.strath.ac.uk/~conor/"
  - name: "Wouter Swierstra"
    link: "http://www.cse.chalmers.se/~wouter/"
  year: "2007"
  doi: "http://doi.acm.org/10.1145/1292597.1292608"
  links:
    doi: "http://doi.acm.org/10.1145/1292597.1292608"
  researchr: "https://researchr.org/publication/AltenkirchMS07"
  cites: 0
  citedby: 0
  pages: "57-68"
  booktitle: "plpv"
  kind: "inproceedings"
  key: "AltenkirchMS07"
- title: "Agda Meets Accelerate"
  author:
  - name: "Peter Thiemann"
    link: "https://researchr.org/alias/peter-thiemann"
  - name: "Manuel M. T. Chakravarty"
    link: "https://researchr.org/alias/manuel-m.-t.-chakravarty"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/978-3-642-41582-1_11"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-41582-1_11"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ifl/ThiemannC12"
  researchr: "https://researchr.org/publication/ThiemannC12"
  cites: 0
  citedby: 0
  pages: "174-189"
  booktitle: "IFL"
  kind: "inproceedings"
  key: "ThiemannC12"
- title: "Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control"
  author:
  - name: "Fahad F. Alhabardi"
    link: "https://researchr.org/alias/fahad-f.-alhabardi"
  - name: "Arnold Beckmann"
    link: "https://researchr.org/alias/arnold-beckmann"
  - name: "Bogdan Lazar"
    link: "https://researchr.org/alias/bogdan-lazar"
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  year: "2021"
  doi: "https://doi.org/10.4230/LIPIcs.TYPES.2021.1"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.TYPES.2021.1"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/types/AlhabardiBLS21"
  researchr: "https://researchr.org/publication/AlhabardiBLS21"
  cites: 0
  citedby: 0
  booktitle: "TYPES"
  kind: "inproceedings"
  key: "AlhabardiBLS21"
- title: "A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family"
  author:
  - name: "Nils Anders Danielsson"
    link: "https://researchr.org/alias/nils-anders-danielsson"
  year: "2006"
  doi: "http://dx.doi.org/10.1007/978-3-540-74464-1_7"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-540-74464-1_7"
  researchr: "https://researchr.org/publication/Danielsson06"
  cites: 0
  citedby: 0
  pages: "93-109"
  booktitle: "TYPES"
  kind: "inproceedings"
  key: "Danielsson06"
- title: "Partiality and Container Monads"
  author:
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  year: "2017"
  doi: "https://doi.org/10.1007/978-3-319-71237-6_20"
  links:
    doi: "https://doi.org/10.1007/978-3-319-71237-6_20"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/aplas/UustaluV17"
  researchr: "https://researchr.org/publication/UustaluV17-1"
  cites: 0
  citedby: 0
  pages: "406-425"
  booktitle: "aplas"
  kind: "inproceedings"
  key: "UustaluV17-1"
- title: "Asynchronous convergence of policy-rich distributed bellman-ford routing protocols"
  author:
  - name: "Matthew L. Daggitt"
    link: "https://researchr.org/alias/matthew-l.-daggitt"
  - name: "Alexander J. T. Gurney"
    link: "https://researchr.org/alias/alexander-j.-t.-gurney"
  - name: "Timothy G. Griffin"
    link: "https://researchr.org/alias/timothy-g.-griffin"
  year: "2018"
  doi: "https://doi.org/10.1145/3230543.3230561"
  links:
    doi: "https://doi.org/10.1145/3230543.3230561"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sigcomm/DaggittGG18"
  researchr: "https://researchr.org/publication/DaggittGG18"
  cites: 0
  citedby: 0
  pages: "103-116"
  booktitle: "sigcomm"
  kind: "inproceedings"
  key: "DaggittGG18"
- title: "Applications of applicative proof search"
  author:
  - name: "Liam O'Connor"
    link: "https://researchr.org/alias/liam-o%27connor"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2976022.2976030"
  links:
    doi: "http://doi.acm.org/10.1145/2976022.2976030"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/OConnor16"
  researchr: "https://researchr.org/publication/OConnor16-0"
  cites: 0
  citedby: 0
  pages: "43-55"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "OConnor16-0"
- title: "Agda-curious?: an exploration of programming with dependent types"
  author:
  - name: "Conor Thomas McBride"
    link: "https://researchr.org/alias/conor-thomas-mcbride"
  year: "2012"
  doi: "http://doi.acm.org/10.1145/2364527.2364529"
  links:
    doi: "http://doi.acm.org/10.1145/2364527.2364529"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/McBride12"
  researchr: "https://researchr.org/publication/McBride12-0"
  cites: 0
  citedby: 0
  pages: "1-2"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "McBride12-0"
- title: "Higher Homotopies in a Hierarchy of Univalent Universes"
  author:
  - name: "Nicolai Kraus"
    link: "https://researchr.org/alias/nicolai-kraus"
  - name: "Christian Sattler"
    link: "https://researchr.org/alias/christian-sattler"
  year: "2015"
  doi: "http://doi.acm.org/10.1145/2729979"
  links:
    doi: "http://doi.acm.org/10.1145/2729979"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/tocl/KrausS15"
  researchr: "https://researchr.org/publication/KrausS15"
  cites: 0
  citedby: 0
  journal: "tocl"
  volume: "16"
  number: "2"
  pages: "18"
  kind: "article"
  key: "KrausS15"
- title: "Eilenberg-MacLane spaces in homotopy type theory"
  author:
  - name: "Daniel R. Licata"
    link: "https://researchr.org/alias/daniel-r.-licata"
  - name: "Eric Finster"
    link: "https://researchr.org/alias/eric-finster"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2603088.2603153"
  links:
    doi: "http://doi.acm.org/10.1145/2603088.2603153"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/LicataF14"
  researchr: "https://researchr.org/publication/LicataF14-0"
  cites: 0
  citedby: 0
  pages: "66"
  booktitle: "csl"
  kind: "inproceedings"
  key: "LicataF14-0"
- title: "Generic constructors and eliminators from descriptions: type theory as a dependently typed internal DSL"
  author:
  - name: "Larry Diehl"
    link: "https://researchr.org/alias/larry-diehl"
  - name: "Tim Sheard"
    link: "https://researchr.org/alias/tim-sheard"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2633628.2633630"
  links:
    doi: "http://doi.acm.org/10.1145/2633628.2633630"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/DiehlS14"
  researchr: "https://researchr.org/publication/DiehlS14"
  cites: 0
  citedby: 0
  pages: "3-14"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "DiehlS14"
- title: "Relative Monads Formalised"
  author:
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  - name: "James Chapman"
    link: "https://researchr.org/alias/james-chapman"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  year: "2014"
  doi: "http://dx.doi.org/10.6092/issn.1972-5787/4389"
  links:
    doi: "http://dx.doi.org/10.6092/issn.1972-5787/4389"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfrea/AltenkirchCU14"
  researchr: "https://researchr.org/publication/AltenkirchCU14"
  cites: 0
  citedby: 0
  journal: "jfrea"
  volume: "7"
  number: "1"
  pages: "1-43"
  kind: "article"
  key: "AltenkirchCU14"
- title: "The Delay Monad and Restriction Categories"
  author:
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  year: "2017"
  doi: "https://doi.org/10.1007/978-3-319-67729-3_3"
  links:
    doi: "https://doi.org/10.1007/978-3-319-67729-3_3"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ictac/UustaluV17"
  researchr: "https://researchr.org/publication/UustaluV17-0"
  cites: 0
  citedby: 0
  pages: "32-50"
  booktitle: "ictac"
  kind: "inproceedings"
  key: "UustaluV17-0"
- title: "Non-Wellfounded Trees in Homotopy Type Theory"
  author:
  - name: "Benedikt Ahrens"
    link: "https://researchr.org/alias/benedikt-ahrens"
  - name: "Paolo Capriotti"
    link: "https://researchr.org/alias/paolo-capriotti"
  - name: "Régis Spadotti"
    link: "https://researchr.org/alias/r%C3%A9gis-spadotti"
  year: "2015"
  doi: "http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.17"
  links:
    doi: "http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.17"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tlca/AhrensCS15"
  researchr: "https://researchr.org/publication/AhrensCS15"
  cites: 0
  citedby: 0
  pages: "17-30"
  booktitle: "tlca"
  kind: "inproceedings"
  key: "AhrensCS15"
- title: "Agda Formalization of a Security-preserving Translation from Flow-sensitive to Flow-insensitive Security Types"
  author:
  - name: "Cecilia Manzino"
    link: "https://researchr.org/alias/cecilia-manzino"
  - name: "Alberto Pardo"
    link: "https://researchr.org/alias/alberto-pardo"
  year: "2020"
  doi: "https://doi.org/10.1016/j.entcs.2020.08.005"
  links:
    doi: "https://doi.org/10.1016/j.entcs.2020.08.005"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lsfa/ManzinoP20"
  researchr: "https://researchr.org/publication/ManzinoP20"
  cites: 0
  citedby: 0
  pages: "75-94"
  booktitle: "LSFA"
  kind: "inproceedings"
  key: "ManzinoP20"
- title: "A calculus for Esterel: if can, can. if no can, no can"
  author:
  - name: "Spencer P. Florence"
    link: "https://researchr.org/alias/spencer-p.-florence"
  - name: "Shu-Hung You"
    link: "https://researchr.org/alias/shu-hung-you"
  - name: "Jesse A. Tov"
    link: "https://researchr.org/alias/jesse-a.-tov"
  - name: "Robert Bruce Findler"
    link: "https://researchr.org/alias/robert-bruce-findler"
  year: "2019"
  doi: "https://dl.acm.org/citation.cfm?id=3290374"
  links:
    doi: "https://dl.acm.org/citation.cfm?id=3290374"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/FlorenceYTF19"
  researchr: "https://researchr.org/publication/FlorenceYTF19"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "3"
  kind: "article"
  key: "FlorenceYTF19"
- title: "The power of Pi"
  author:
  - name: "Nicolas Oury"
    link: "http://www.inf.ed.ac.uk/people/staff/Nicholas_Oury.html"
  - name: "Wouter Swierstra"
    link: "http://www.cse.chalmers.se/~wouter/"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1411204.1411213"
  links:
    doi: "http://doi.acm.org/10.1145/1411204.1411213"
  researchr: "https://researchr.org/publication/OuryS08"
  cites: 0
  citedby: 0
  pages: "39-50"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "OuryS08"
- title: "Formal metatheory of second-order abstract syntax"
  author:
  - name: "Marcelo Fiore"
    link: "https://researchr.org/alias/marcelo-fiore"
  - name: "Dmitrij Szamozvancev"
    link: "https://researchr.org/alias/dmitrij-szamozvancev"
  year: "2022"
  doi: "https://doi.org/10.1145/3498715"
  links:
    doi: "https://doi.org/10.1145/3498715"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/FioreS22"
  researchr: "https://researchr.org/publication/FioreS22"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "6"
  number: "POPL"
  pages: "1-29"
  kind: "article"
  key: "FioreS22"
- title: "Certified Parsing of Regular Languages"
  author:
  - name: "Denis Firsov"
    link: "https://researchr.org/alias/denis-firsov"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  year: "2013"
  doi: "http://dx.doi.org/10.1007/978-3-319-03545-1_7"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-03545-1_7"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/FirsovU13"
  researchr: "https://researchr.org/publication/FirsovU13"
  cites: 0
  citedby: 0
  pages: "98-113"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "FirsovU13"
- title: "Overlapping and Order-Independent Patterns - Definitional Equality for All"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-642-54833-8_6"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-54833-8_6"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/CockxPD14"
  researchr: "https://researchr.org/publication/CockxPD14"
  cites: 0
  citedby: 0
  pages: "87-106"
  booktitle: "ESOP"
  kind: "inproceedings"
  key: "CockxPD14"
- title: "From fine- to coarse-grained dynamic information flow control and back"
  author:
  - name: "Marco Vassena"
    link: "https://researchr.org/alias/marco-vassena"
  - name: "Alejandro Russo"
    link: "https://researchr.org/alias/alejandro-russo"
  - name: "Deepak Garg"
    link: "https://people.mpi-sws.org/~dg/"
  - name: "Vineet Rajani"
    link: "https://researchr.org/alias/vineet-rajani"
  - name: "Deian Stefan"
    link: "https://researchr.org/alias/deian-stefan"
  year: "2019"
  doi: "https://dl.acm.org/citation.cfm?id=3290389"
  links:
    doi: "https://dl.acm.org/citation.cfm?id=3290389"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/VassenaRGRS19"
  researchr: "https://researchr.org/publication/VassenaRGRS19"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "3"
  kind: "article"
  key: "VassenaRGRS19"
- title: "Intrinsically Correct Sorting in Cubical Agda"
  author:
  - name: "Cass Alexandru"
    link: "https://researchr.org/alias/cass-alexandru"
  - name: "Vikraman Choudhury"
    link: "https://researchr.org/alias/vikraman-choudhury"
  - name: "Jurriaan Rot"
    link: "https://researchr.org/alias/jurriaan-rot"
  - name: "Niels van der Weide"
    link: "https://researchr.org/alias/niels-van-der-weide"
  year: "2025"
  doi: "https://doi.org/10.1145/3703595.3705873"
  links:
    doi: "https://doi.org/10.1145/3703595.3705873"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/AlexandruCRW25"
  researchr: "https://researchr.org/publication/AlexandruCRW25"
  cites: 0
  citedby: 0
  pages: "34-49"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "AlexandruCRW25"
- title: "Integrity Constraints for Linked Data"
  author:
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  - name: "Peter F. Patel-Schneider"
    link: "https://researchr.org/alias/peter-f.-patel-schneider"
  year: "2011"
  doi: "http://ceur-ws.org/Vol-745/paper_31.pdf"
  links:
    doi: "http://ceur-ws.org/Vol-745/paper_31.pdf"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/dlog/JeffreyP11"
  tags:
  - "constraints"
  - "data-flow"
  researchr: "https://researchr.org/publication/JeffreyP11"
  cites: 0
  citedby: 0
  booktitle: "dlog"
  kind: "inproceedings"
  key: "JeffreyP11"
- title: "Internalizing representation independence with univalence"
  author:
  - name: "Carlo Angiuli"
    link: "https://researchr.org/alias/carlo-angiuli"
  - name: "Evan Cavallo"
    link: "https://researchr.org/alias/evan-cavallo"
  - name: "Anders Mörtberg"
    link: "https://researchr.org/alias/anders-m%C3%B6rtberg"
  - name: "Max Zeuner"
    link: "https://researchr.org/alias/max-zeuner"
  year: "2021"
  doi: "https://doi.org/10.1145/3434293"
  links:
    doi: "https://doi.org/10.1145/3434293"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/AngiuliCMZ21"
  researchr: "https://researchr.org/publication/AngiuliCMZ21"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "5"
  number: "POPL"
  pages: "1-30"
  kind: "article"
  key: "AngiuliCMZ21"
- title: "Functions out of Higher Truncations"
  author:
  - name: "Paolo Capriotti"
    link: "https://researchr.org/alias/paolo-capriotti"
  - name: "Nicolai Kraus"
    link: "https://researchr.org/alias/nicolai-kraus"
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  year: "2015"
  doi: "http://dx.doi.org/10.4230/LIPIcs.CSL.2015.359"
  links:
    doi: "http://dx.doi.org/10.4230/LIPIcs.CSL.2015.359"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/CapriottiKV15"
  researchr: "https://researchr.org/publication/CapriottiKV15"
  cites: 0
  citedby: 0
  pages: "359-373"
  booktitle: "csl"
  kind: "inproceedings"
  key: "CapriottiKV15"
- title: "Agda as a platform for the development of verified railway interlocking systems"
  author:
  - name: "Karim Kanso"
    link: "https://researchr.org/alias/karim-kanso"
  year: "2012"
  doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.678306"
  links:
    doi: "http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.678306"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/ethos/Kanso12"
  researchr: "https://researchr.org/publication/ethos-1592"
  cites: 0
  citedby: 0
  school: "Swansea University, UK"
  kind: "phdthesis"
  key: "ethos-1592"
- title: "Big-step normalisation"
  author:
  - name: "Thorsten Altenkirch"
    link: "http://www.cs.nott.ac.uk/~txa"
  - name: "James Chapman"
    link: "https://researchr.org/alias/james-chapman"
  - name: " "
    link: "https://researchr.org/alias/"
  - name: " "
    link: "https://researchr.org/alias/"
  year: "2009"
  doi: "http://dx.doi.org/10.1017/S0956796809007278"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796809007278"
  researchr: "https://researchr.org/publication/AltenkirchC09"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "19"
  number: "3-4"
  pages: "311-333"
  kind: "article"
  key: "AltenkirchC09"
- title: "Transporting functions across ornaments"
  author:
  - name: "Pierre-Évariste Dagand"
    link: "https://researchr.org/alias/pierre-%C3%A9variste-dagand"
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  year: "2012"
  doi: "http://doi.acm.org/10.1145/2364527.2364544"
  links:
    doi: "http://doi.acm.org/10.1145/2364527.2364544"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/DagandM12"
  researchr: "https://researchr.org/publication/DagandM12"
  cites: 0
  citedby: 0
  pages: "103-114"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "DagandM12"
- title: "Dependently typed programming in Agda"
  author:
  - name: "Ulf Norell"
    link: "http://www.cse.chalmers.se/~ulfn/"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1481861.1481862"
  links:
    doi: "http://doi.acm.org/10.1145/1481861.1481862"
  tags:
  - "programming"
  researchr: "https://researchr.org/publication/Norell09"
  cites: 0
  citedby: 0
  pages: "1-2"
  booktitle: "tldi"
  kind: "inproceedings"
  key: "Norell09"
- title: "Programming and Reasoning with Guarded Recursion for Coinductive Types"
  author:
  - name: "Ranald Clouston"
    link: "https://researchr.org/alias/ranald-clouston"
  - name: "Ales Bizjak"
    link: "https://researchr.org/alias/ales-bizjak"
  - name: "Hans Bugge Grathwohl"
    link: "https://researchr.org/alias/hans-bugge-grathwohl"
  - name: "Lars Birkedal"
    link: "https://researchr.org/alias/lars-birkedal"
  year: "2015"
  doi: "http://dx.doi.org/10.1007/978-3-662-46678-0_26"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-662-46678-0_26"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fossacs/CloustonBGB15"
  researchr: "https://researchr.org/publication/CloustonBGB15"
  cites: 0
  citedby: 0
  pages: "407-421"
  booktitle: "fossacs"
  kind: "inproceedings"
  key: "CloustonBGB15"
- title: "Towards Certifiable Implementation of Graph Transformation via Relation Categories"
  author:
  - name: "Wolfram Kahl"
    link: "https://researchr.org/alias/wolfram-kahl"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/978-3-642-33314-9_6"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-33314-9_6"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/RelMiCS/Kahl12"
  researchr: "https://researchr.org/publication/Kahl12"
  cites: 0
  citedby: 0
  pages: "82-97"
  booktitle: "RelMiCS"
  kind: "inproceedings"
  key: "Kahl12"
- title: "Defining Trace Semantics for CSP-Agda"
  author:
  - name: "Bashar Igried"
    link: "https://researchr.org/alias/bashar-igried"
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  year: "2016"
  doi: "https://doi.org/10.4230/LIPIcs.TYPES.2016.12"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.TYPES.2016.12"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/types/IgriedS16"
  researchr: "https://researchr.org/publication/IgriedS16-0"
  cites: 0
  citedby: 0
  booktitle: "TYPES"
  kind: "inproceedings"
  key: "IgriedS16-0"
- title: "3) ≅Z/2Z and Computing a Brunerie Number in Cubical Agda"
  author:
  - name: "Axel Ljungström"
    link: "https://researchr.org/alias/axel-ljungstr%C3%B6m"
  - name: "Anders Mörtberg"
    link: "https://researchr.org/alias/anders-m%C3%B6rtberg"
  year: "2023"
  doi: "https://doi.org/10.1109/LICS56636.2023.10175833"
  links:
    doi: "https://doi.org/10.1109/LICS56636.2023.10175833"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/LjungstromM23"
  researchr: "https://researchr.org/publication/LjungstromM23"
  cites: 0
  citedby: 0
  pages: "1-13"
  booktitle: "lics"
  kind: "inproceedings"
  key: "LjungstromM23"
- title: "Flexible Coinduction in Agda"
  author:
  - name: "Luca Ciccone"
    link: "https://researchr.org/alias/luca-ciccone"
  - name: "Francesco Dagnino"
    link: "https://researchr.org/alias/francesco-dagnino"
  - name: "Elena Zucca"
    link: "https://researchr.org/alias/elena-zucca"
  year: "2021"
  doi: "https://doi.org/10.4230/LIPIcs.ITP.2021.13"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.ITP.2021.13"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/CicconeDZ21"
  researchr: "https://researchr.org/publication/CicconeDZ21"
  cites: 0
  citedby: 0
  booktitle: "itp"
  kind: "inproceedings"
  key: "CicconeDZ21"
- title: "π-calculus in Guarded Cubical Agda"
  author:
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  year: "2023"
  month: "February"
  doi: "https://doi.org/10.1016/j.jlamp.2022.100846"
  links:
    doi: "https://doi.org/10.1016/j.jlamp.2022.100846"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jlap/VeltriV23"
  researchr: "https://researchr.org/publication/VeltriV23"
  cites: 0
  citedby: 0
  journal: "jlap"
  volume: "131"
  pages: "100846"
  kind: "article"
  key: "VeltriV23"
- title: "Sikkel: Multimode Simple Type Theory as an Agda Library"
  author:
  - name: "Joris Ceulemans"
    link: "https://researchr.org/alias/joris-ceulemans"
  - name: "Andreas Nuyts"
    link: "https://researchr.org/alias/andreas-nuyts"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2022"
  month: "jun"
  doi: "10.4204/eptcs.360.5"
  links:
    "url": "https://doi.org/10.4204%2Feptcs.360.5"
  researchr: "https://researchr.org/publication/Ceulemans2022"
  cites: 0
  citedby: 0
  journal: "Electronic Proceedings in Theoretical Computer Science"
  volume: "360"
  pages: "93-112"
  kind: "article"
  key: "Ceulemans2022"
- title: "Positive Inductive-Recursive Definitions"
  author:
  - name: "Neil Ghani"
    link: "https://researchr.org/alias/neil-ghani"
  - name: "Lorenzo Malatesta"
    link: "https://researchr.org/alias/lorenzo-malatesta"
  - name: "Fredrik Nordvall Forsberg"
    link: "https://researchr.org/alias/fredrik-nordvall-forsberg"
  year: "2013"
  doi: "http://dx.doi.org/10.1007/978-3-642-40206-7_3"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-40206-7_3"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/calco/GhaniMF13"
  researchr: "https://researchr.org/publication/GhaniMF13"
  cites: 0
  citedby: 0
  pages: "19-33"
  booktitle: "calco"
  kind: "inproceedings"
  key: "GhaniMF13"
- title: "Undecidability of d<: and its decidable fragments"
  author:
  - name: "Jason Z. S. Hu"
    link: "https://researchr.org/alias/jason-z.-s.-hu"
  - name: "Ondrej Lhoták"
    link: "https://researchr.org/alias/ondrej-lhot%C3%A1k"
  year: "2020"
  doi: "https://doi.org/10.1145/3371077"
  links:
    doi: "https://doi.org/10.1145/3371077"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/HuL20"
  researchr: "https://researchr.org/publication/HuL20"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "4"
  number: "POPL"
  kind: "article"
  key: "HuL20"
- title: "Extracting a call-by-name partial evaluator from a proof of termination"
  author:
  - name: "Kenichi Asai"
    link: "https://researchr.org/alias/kenichi-asai"
  year: "2019"
  doi: "https://doi.org/10.1145/3294032.3294084"
  links:
    doi: "https://doi.org/10.1145/3294032.3294084"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pepm/Asai19"
  researchr: "https://researchr.org/publication/Asai19"
  cites: 0
  citedby: 0
  pages: "61-67"
  booktitle: "PEPM"
  kind: "inproceedings"
  key: "Asai19"
- title: "Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation"
  author:
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863495.1863497"
  links:
    doi: "http://doi.acm.org/10.1145/1863495.1863497"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/McBride10"
  researchr: "https://researchr.org/publication/McBride10-0"
  cites: 0
  citedby: 0
  pages: "1-12"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "McBride10-0"
- title: "Simple noninterference from parametricity"
  author:
  - name: "Maximilian Algehed"
    link: "https://researchr.org/alias/maximilian-algehed"
  - name: "Jean-Philippe Bernardy"
    link: "https://researchr.org/alias/jean-philippe-bernardy"
  year: "2019"
  doi: "https://doi.org/10.1145/3341693"
  links:
    doi: "https://doi.org/10.1145/3341693"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/AlgehedB19"
  researchr: "https://researchr.org/publication/AlgehedB19"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "3"
  number: "ICFP"
  kind: "article"
  key: "AlgehedB19"
- title: "Axioms for Modelling Cubical Type Theory in a Topos"
  author:
  - name: "Ian Orton"
    link: "https://researchr.org/alias/ian-orton"
  - name: "Andrew M. Pitts"
    link: "https://researchr.org/alias/andrew-m.-pitts"
  year: "2018"
  doi: "https://doi.org/10.23638/LMCS-14(4:23)2018"
  links:
    doi: "https://doi.org/10.23638/LMCS-14(4:23)2018"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/lmcs/OrtonP18"
  researchr: "https://researchr.org/publication/OrtonP18"
  cites: 0
  citedby: 0
  journal: "lmcs"
  volume: "14"
  number: "4"
  kind: "article"
  key: "OrtonP18"
- title: "On Formalizing Information-Flow Control Libraries"
  author:
  - name: "Marco Vassena"
    link: "https://researchr.org/alias/marco-vassena"
  - name: "Alejandro Russo"
    link: "https://researchr.org/alias/alejandro-russo"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2993600.2993608"
  links:
    doi: "http://doi.acm.org/10.1145/2993600.2993608"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ccs/VassenaR16"
  researchr: "https://researchr.org/publication/VassenaR16"
  cites: 0
  citedby: 0
  pages: "15-28"
  booktitle: "ccs"
  kind: "inproceedings"
  key: "VassenaR16"
- title: "Decidability of conversion for type theory in type theory"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Joakim Öhman"
    link: "https://researchr.org/alias/joakim-%C3%B6hman"
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  year: "2018"
  doi: "http://doi.acm.org/10.1145/3158111"
  links:
    doi: "http://doi.acm.org/10.1145/3158111"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/0001OV18"
  researchr: "https://researchr.org/publication/0001OV18"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "2"
  number: "POPL"
  kind: "article"
  key: "0001OV18"
- title: "A type and scope safe universe of syntaxes with binding: their semantics and proofs"
  author:
  - name: "Guillaume Allais"
    link: "https://researchr.org/alias/guillaume-allais"
  - name: "Robert Atkey"
    link: "https://researchr.org/alias/robert-atkey"
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Conor McBride"
    link: "http://personal.cis.strath.ac.uk/~conor/"
  - name: "James McKinna"
    link: "https://researchr.org/alias/james-mckinna"
  year: "2018"
  doi: "https://doi.org/10.1145/3236785"
  links:
    doi: "https://doi.org/10.1145/3236785"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/AllaisA0MM18"
  researchr: "https://researchr.org/publication/AllaisA0MM18"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "2"
  number: "ICFP"
  kind: "article"
  key: "AllaisA0MM18"
- 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: "Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Orestis Melkonian"
    link: "https://researchr.org/alias/orestis-melkonian"
  - name: "Lucas Escot"
    link: "https://researchr.org/alias/lucas-escot"
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Ulf Norell"
    link: "https://researchr.org/alias/ulf-norell"
  year: "2022"
  doi: "https://doi.org/10.1145/3546189.3549920"
  links:
    doi: "https://doi.org/10.1145/3546189.3549920"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/haskell/CockxME0N22"
  researchr: "https://researchr.org/publication/CockxME0N22"
  cites: 0
  citedby: 0
  pages: "108-122"
  booktitle: "haskell"
  kind: "inproceedings"
  key: "CockxME0N22"
- title: "Higher-order Games with Dependent Types"
  author:
  - name: "Escardo, Martin"
    link: "https://researchr.org/alias/escardo%2C-martin"
  - name: "Oliva, Paulo"
    link: "https://researchr.org/alias/oliva%2C-paulo"
  year: "2022"
  doi: "10.48550/ARXIV.2212.07735"
  links:
    "url": "https://arxiv.org/abs/2212.07735"
  researchr: "https://researchr.org/publication/https%3A-doi.org-10.48550-arxiv.2212.07735"
  cites: 0
  citedby: 0
  kind: "misc"
  key: "https:-doi.org-10.48550-arxiv.2212.07735"
- title: "Two set-based implementations of quotients in type theory"
  author:
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  year: "2015"
  doi: "http://ceur-ws.org/Vol-1525/paper-14.pdf"
  links:
    doi: "http://ceur-ws.org/Vol-1525/paper-14.pdf"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/splst/Veltri15"
  researchr: "https://researchr.org/publication/Veltri15"
  cites: 0
  citedby: 0
  pages: "194-205"
  booktitle: "splst"
  kind: "inproceedings"
  key: "Veltri15"
- title: "Normalisation by Evaluation for Dependent Types"
  author:
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  - name: "Ambrus Kaposi"
    link: "https://researchr.org/alias/ambrus-kaposi"
  year: "2016"
  doi: "http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.6"
  links:
    doi: "http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.6"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/rta/AltenkirchK16"
  researchr: "https://researchr.org/publication/AltenkirchK16-0"
  cites: 0
  citedby: 0
  booktitle: "RTA"
  kind: "inproceedings"
  key: "AltenkirchK16-0"
- title: "Calculating a linear-time solution to the densest-segment problem"
  author:
  - name: "Sharon A. Curtis"
    link: "https://researchr.org/alias/sharon-a.-curtis"
  - name: "Shin-Cheng Mu"
    link: "https://researchr.org/alias/shin-cheng-mu"
  year: "2015"
  doi: "http://dx.doi.org/10.1017/S095679681500026X"
  links:
    doi: "http://dx.doi.org/10.1017/S095679681500026X"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/CurtisM15"
  researchr: "https://researchr.org/publication/CurtisM15"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "25"
  kind: "article"
  key: "CurtisM15"
- title: "Guarded Recursion in Agda via Sized Types"
  author:
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  - name: "Niels van der Weide"
    link: "https://researchr.org/alias/niels-van-der-weide"
  year: "2019"
  doi: "https://doi.org/10.4230/LIPIcs.FSCD.2019.32"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.FSCD.2019.32"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/rta/VeltriW19"
  researchr: "https://researchr.org/publication/VeltriW19"
  cites: 0
  citedby: 0
  booktitle: "RTA"
  kind: "inproceedings"
  key: "VeltriW19"
- title: "A light-weight integration of automated and interactive theorem proving"
  author:
  - name: "Karim Kanso"
    link: "https://researchr.org/alias/karim-kanso"
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  year: "2016"
  doi: "http://dx.doi.org/10.1017/S0960129514000140"
  links:
    doi: "http://dx.doi.org/10.1017/S0960129514000140"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/mscs/KansoS16"
  researchr: "https://researchr.org/publication/KansoS16"
  cites: 0
  citedby: 0
  journal: "mscs"
  volume: "26"
  number: "1"
  pages: "129-153"
  kind: "article"
  key: "KansoS16"
- title: "A Categorical Treatment of Ornaments"
  author:
  - name: "Pierre-Évariste Dagand"
    link: "https://researchr.org/alias/pierre-%C3%A9variste-dagand"
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  year: "2013"
  doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2013.60"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2013.60"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/DagandM13"
  researchr: "https://researchr.org/publication/DagandM13"
  cites: 0
  citedby: 0
  pages: "530-539"
  booktitle: "lics"
  kind: "inproceedings"
  key: "DagandM13"
- title: "Some constructions on ω-groupoids"
  author:
  - name: "Thorsten Altenkirch"
    link: "https://researchr.org/alias/thorsten-altenkirch"
  - name: "Nuo Li"
    link: "https://researchr.org/alias/nuo-li"
  - name: "Ondrej Rypacek"
    link: "https://researchr.org/alias/ondrej-rypacek"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2631172.2631176"
  links:
    doi: "http://doi.acm.org/10.1145/2631172.2631176"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lfmtp/AltenkirchLR14"
  researchr: "https://researchr.org/publication/AltenkirchLR14"
  cites: 0
  citedby: 0
  booktitle: "lfmtp"
  kind: "inproceedings"
  key: "AltenkirchLR14"
- title: "Quotienting the Delay Monad by Weak Bisimilarity"
  author:
  - name: "James Chapman"
    link: "https://researchr.org/alias/james-chapman"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  - name: "Niccolò Veltri"
    link: "https://researchr.org/alias/niccol%C3%B2-veltri"
  year: "2015"
  doi: "http://dx.doi.org/10.1007/978-3-319-25150-9_8"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-25150-9_8"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ictac/ChapmanUV15"
  researchr: "https://researchr.org/publication/ChapmanUV15"
  cites: 0
  citedby: 0
  pages: "110-125"
  booktitle: "ictac"
  kind: "inproceedings"
  key: "ChapmanUV15"
- title: "Generic lookup and update for infinitary inductive-recursive types"
  author:
  - name: "Larry Diehl"
    link: "https://researchr.org/alias/larry-diehl"
  - name: "Tim Sheard"
    link: "https://researchr.org/alias/tim-sheard"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2976022.2976031"
  links:
    doi: "http://doi.acm.org/10.1145/2976022.2976031"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/DiehlS16"
  researchr: "https://researchr.org/publication/DiehlS16"
  cites: 0
  citedby: 0
  pages: "1-12"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "DiehlS16"
- title: "Parametric quantifiers for dependent type theory"
  author:
  - name: "Andreas Nuyts"
    link: "https://researchr.org/alias/andreas-nuyts"
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3110276"
  links:
    doi: "http://doi.acm.org/10.1145/3110276"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/NuytsVD17"
  researchr: "https://researchr.org/publication/NuytsVD17"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "1"
  number: "ICFP"
  kind: "article"
  key: "NuytsVD17"
- title: "Intrinsically-typed definitional interpreters à la carte"
  author:
  - name: "Cas van der Rest"
    link: "https://researchr.org/alias/cas-van-der-rest"
  - name: "Casper Bach Poulsen"
    link: "http://www.casperbp.net"
  - name: "Arjen Rouvoet"
    link: "https://researchr.org/alias/arjen-rouvoet"
  - name: "Eelco Visser"
    link: "https://researchr.org/alias/eelco-visser"
  - name: "Peter D. Mosses"
    link: "https://researchr.org/alias/peter-d.-mosses"
  year: "2022"
  doi: "https://doi.org/10.1145/3563355"
  links:
    doi: "https://doi.org/10.1145/3563355"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/RestPRVM22"
  researchr: "https://researchr.org/publication/RestPRVM22"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "6"
  number: "OOPSLA2"
  pages: "1903-1932"
  kind: "article"
  key: "RestPRVM22"
- title: "A formalisation of LEGv8 in Agda"
  author:
  - name: "Santiago Arranz Olmos"
    link: "https://researchr.org/alias/santiago-arranz-olmos"
  - name: "Martín-Fernández"
    link: "https://researchr.org/alias/mart%C3%ADn-fern%C3%A1ndez"
  - name: "Matías Steinberg"
    link: "https://researchr.org/alias/mat%C3%ADas-steinberg"
  - name: "Alejandro Gadea"
    link: "https://researchr.org/alias/alejandro-gadea"
  - name: "Emmanuel Gunther"
    link: "https://researchr.org/alias/emmanuel-gunther"
  - name: "Miguel Pagano"
    link: "https://researchr.org/alias/miguel-pagano"
  year: "2020"
  doi: "https://doi.org/10.1145/3427081.3427086"
  links:
    doi: "https://doi.org/10.1145/3427081.3427086"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sblp/OlmosFSGGP20"
  researchr: "https://researchr.org/publication/OlmosFSGGP20"
  cites: 0
  citedby: 0
  pages: "33-39"
  booktitle: "SBLP"
  kind: "inproceedings"
  key: "OlmosFSGGP20"
- title: "Certified Foata Normalization for Generalized Traces"
  author:
  - name: "Hendrik Maarand"
    link: "https://researchr.org/alias/hendrik-maarand"
  - name: "Tarmo Uustalu"
    link: "https://researchr.org/alias/tarmo-uustalu"
  year: "2018"
  doi: "https://doi.org/10.1007/978-3-319-77935-5_21"
  links:
    doi: "https://doi.org/10.1007/978-3-319-77935-5_21"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/nfm/MaarandU18"
  researchr: "https://researchr.org/publication/MaarandU18"
  cites: 0
  citedby: 0
  pages: "299-314"
  booktitle: "NFM"
  kind: "inproceedings"
  key: "MaarandU18"
- title: "Work it, wrap it, fix it, fold it"
  author:
  - name: "Neil Sculthorpe"
    link: "https://researchr.org/alias/neil-sculthorpe"
  - name: "Graham Hutton"
    link: "https://researchr.org/alias/graham-hutton"
  year: "2014"
  doi: "http://dx.doi.org/10.1017/S0956796814000045"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796814000045"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/SculthorpeH14"
  researchr: "https://researchr.org/publication/SculthorpeH14"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "24"
  number: "1"
  pages: "113-127"
  kind: "article"
  key: "SculthorpeH14"
- title: "Namely, Painless: A unifying approach to safe programming with first-order syntax with binders. (Une approche unifiante pour programmer sûrement avec de la syntaxe du premier ordre contenant des lieurs)"
  author:
  - name: "Nicolas Pouillard"
    link: "https://researchr.org/alias/nicolas-pouillard"
  year: "2012"
  doi: "https://tel.archives-ouvertes.fr/tel-00759059"
  links:
    doi: "https://tel.archives-ouvertes.fr/tel-00759059"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/hal/Pouillard12"
  researchr: "https://researchr.org/publication/hal-3916"
  cites: 0
  citedby: 0
  school: "Paris Diderot University, France"
  kind: "phdthesis"
  key: "hal-3916"
- title: "Initial Algebras Unchained - A Novel Initial Algebra Construction Formalized in Agda"
  author:
  - name: "Thorsten Wißmann"
    link: "https://researchr.org/alias/thorsten-wi%C3%9Fmann"
  - name: "Stefan Milius"
    link: "https://researchr.org/alias/stefan-milius"
  year: "2024"
  doi: "https://doi.org/10.1145/3661814.3662105"
  links:
    doi: "https://doi.org/10.1145/3661814.3662105"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/WissmannM24"
  researchr: "https://researchr.org/publication/WissmannM24"
  cites: 0
  citedby: 0
  booktitle: "lics"
  kind: "inproceedings"
  key: "WissmannM24"
- title: "Bag Equivalence via a Proof-Relevant Membership Relation"
  author:
  - name: "Nils Anders Danielsson"
    link: "https://researchr.org/alias/nils-anders-danielsson"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/978-3-642-32347-8_11"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-32347-8_11"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/Danielsson12"
  researchr: "https://researchr.org/publication/Danielsson12"
  cites: 0
  citedby: 0
  pages: "149-165"
  booktitle: "itp"
  kind: "inproceedings"
  key: "Danielsson12"
- title: "A formal framework for heterogeneous systems semantics. (Un environnement formel pour la sémantique des systèmes hétérogènes)"
  author:
  - name: "Mathieu Montin"
    link: "https://researchr.org/alias/mathieu-montin"
  year: "2020"
  doi: "https://tel.archives-ouvertes.fr/tel-04169893"
  links:
    doi: "https://tel.archives-ouvertes.fr/tel-04169893"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/hal/Montin20"
  researchr: "https://researchr.org/publication/hal-19381"
  cites: 0
  citedby: 0
  school: "National Polytechnic Institute of Toulouse, France"
  kind: "phdthesis"
  key: "hal-19381"
- title: "New equations for neutral terms: a sound and complete decision procedure, formalized"
  author:
  - name: "Guillaume Allais"
    link: "https://researchr.org/alias/guillaume-allais"
  - name: "Conor McBride"
    link: "https://researchr.org/alias/conor-mcbride"
  - name: "Pierre Boutillier"
    link: "https://researchr.org/alias/pierre-boutillier"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2502409.2502411"
  links:
    doi: "http://doi.acm.org/10.1145/2502409.2502411"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/AllaisMB13"
  researchr: "https://researchr.org/publication/AllaisMB13"
  cites: 0
  citedby: 0
  pages: "13-24"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "AllaisMB13"
- title: "System F in Agda, for Fun and Profit"
  author:
  - name: "James Chapman"
    link: "https://iohk.io/en/team/james-chapman"
  - name: "Roman Kireev"
    link: "https://researchr.org/alias/roman-kireev"
  - name: "Chad Nester"
    link: "https://researchr.org/alias/chad-nester"
  - name: "Philip Wadler"
    link: "http://homepages.inf.ed.ac.uk/wadler/"
  year: "2019"
  doi: "https://doi.org/10.1007/978-3-030-33636-3_10"
  links:
    doi: "https://doi.org/10.1007/978-3-030-33636-3_10"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/mpc/ChapmanKNW19"
  tags:
  - "Intrinsic-Verification"
  researchr: "https://researchr.org/publication/ChapmanKNW19"
  cites: 0
  citedby: 0
  pages: "255-297"
  booktitle: "mpc"
  kind: "inproceedings"
  key: "ChapmanKNW19"
- title: "Practical generic programming over a universe of native datatypes"
  author:
  - name: "Lucas Escot"
    link: "https://researchr.org/alias/lucas-escot"
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  year: "2022"
  doi: "https://doi.org/10.1145/3547644"
  links:
    doi: "https://doi.org/10.1145/3547644"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/EscotC22"
  researchr: "https://researchr.org/publication/EscotC22"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "6"
  number: "ICFP"
  pages: "625-649"
  kind: "article"
  key: "EscotC22"
- title: "Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic"
  author:
  - name: "Guillaume Allais"
    link: "https://researchr.org/alias/guillaume-allais"
  year: "2017"
  doi: "https://doi.org/10.4230/LIPIcs.TYPES.2017.1"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.TYPES.2017.1"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/types/Allais17"
  researchr: "https://researchr.org/publication/Allais17"
  cites: 0
  citedby: 0
  booktitle: "TYPES"
  kind: "inproceedings"
  key: "Allais17"