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: "Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings" editor: - name: "Javier Esparza" link: "https://researchr.org/alias/javier-esparza" - name: "Andrzej S. Murawski" link: "https://researchr.org/alias/andrzej-s.-murawski" volume: "10203" series: "Lecture Notes in Computer Science" isbn: "978-3-662-54458-7" 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: "Relational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014, Marienstatt, Germany, April 28-May 1, 2014. Proceedings" editor: - name: "Peter Höfner" link: "https://researchr.org/alias/peter-h%C3%B6fner" - name: "Peter Jipsen" link: "https://researchr.org/alias/peter-jipsen" - name: "Wolfram Kahl" link: "https://researchr.org/alias/wolfram-kahl" - name: "Martin Eric Müller" link: "https://researchr.org/alias/martin-eric-m%C3%BCller" volume: "8428" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-06250-1" 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: "Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Philadelphia, PA, USA, Saturday, January 28, 2012" editor: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" publisher: "ACM" isbn: "978-1-4503-1120-5" 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: "Proceedings of the ACM on Programming Languages" 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: "30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference)" editor: - name: "Florin Manea" link: "https://researchr.org/alias/florin-manea" - name: "Alex Simpson" link: "https://researchr.org/alias/alex-simpson" volume: "216" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-218-1" 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: "Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings" editor: - name: "Marc Bezem" link: "https://researchr.org/alias/marc-bezem" volume: "12" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-939897-32-3" 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: "Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020" editor: - name: "Jasmin Blanchette" link: "https://researchr.org/alias/jasmin-blanchette" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" publisher: "ACM" isbn: "978-1-4503-7097-4" 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: "Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA" publisher: "IEEE Computer Society" isbn: "978-0-7695-3183-0" 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: "Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016" editor: - name: "Martin Grohe" link: "https://researchr.org/alias/martin-grohe" - name: "Eric Koskinen" link: "https://researchr.org/alias/eric-koskinen" - name: "Natarajan Shankar" link: "https://researchr.org/alias/natarajan-shankar" publisher: "ACM" isbn: "978-1-4503-4391-6" 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: "Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009" editor: - name: "Thorsten Altenkirch" link: "http://www.cs.nott.ac.uk/~txa" - name: "Todd D. Millstein" link: "https://researchr.org/alias/todd-d.-millstein" publisher: "ACM" isbn: "978-1-60558-330-3" 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: "Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA" publisher: "IEEE Computer Society" isbn: "978-0-7695-3746-7" 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: "25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France" editor: - name: "Jean-Marc Talbot" link: "https://researchr.org/alias/jean-marc-talbot" - name: "Laurent Regnier" link: "https://researchr.org/alias/laurent-regnier" volume: "62" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-95977-022-4" kind: "inproceedings" key: "FavoniaS16" - 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: "Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2017, Oxford, UK, September 3, 2017" editor: - name: "Sam Lindley" link: "https://researchr.org/alias/sam-lindley" - name: "Brent A. Yorgey" link: "https://researchr.org/alias/brent-a.-yorgey" publisher: "ACM" isbn: "978-1-4503-5183-6" 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: "Journal of Functional Programming" 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" note: "British Library, EThOS" 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: "13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel" editor: - name: "June Andronick" link: "https://researchr.org/alias/june-andronick" - name: "Leonardo de Moura" link: "https://researchr.org/alias/leonardo-de-moura" volume: "237" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-252-5" 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: "Electronic Notes in Theoretical Computer Science" 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: "Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, 2010" editor: - name: "Cormac Flanagan" link: "https://researchr.org/alias/cormac-flanagan" - name: "Jean-Christophe Filliâtre" link: "https://researchr.org/alias/jean-christophe-filli%C3%A2tre" publisher: "ACM" isbn: "978-1-60558-890-2" 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: "Journal of Functional Programming" 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: "Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures" editor: - name: "Pieter W. M. Koopman" link: "https://researchr.org/alias/pieter-w.-m.-koopman" - name: "Rinus Plasmeijer" link: "https://researchr.org/alias/rinus-plasmeijer" - name: "S. Doaitse Swierstra" link: "http://www.cs.uu.nl/staff/doaitse.html" volume: "5832" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-04651-3" 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: "Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010" editor: - name: "Paul Hudak" link: "https://researchr.org/alias/paul-hudak" - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-60558-794-3" 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: "Proceedings of the ACM on Programming Languages" 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 '20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020" publisher: "ACM" isbn: "978-1-4503-8821-4" 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: "25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France" editor: - name: "Jean-Marc Talbot" link: "https://researchr.org/alias/jean-marc-talbot" - name: "Laurent Regnier" link: "https://researchr.org/alias/laurent-regnier" volume: "62" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-95977-022-4" kind: "inproceedings" key: "OrtonP16" - 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: "Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised Tutorial Lectures" editor: - name: "Ana Bove" link: "https://researchr.org/alias/ana-bove" - name: "Luís Soares Barbosa" link: "https://researchr.org/alias/lu%C3%A3%C2%ADs-soares-barbosa" - name: "Alberto Pardo" link: "https://researchr.org/alias/alberto-pardo" - name: "Jorge Sousa Pinto" link: "https://researchr.org/alias/jorge-sousa-pinto" volume: "5520" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-03152-6" 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: "Proceedings of the ACM on Programming Languages" 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 '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021" editor: - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "Andrei Popescu 0001" link: "https://researchr.org/alias/andrei-popescu-0001" publisher: "ACM" isbn: "978-1-4503-8299-1" 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: "Proceedings of the Tenth Symposium on Trends in Functional Programming, TFP 2009, Komárno, Slovakia, June 2-4, 2009" editor: - name: "Zoltán Horváth" link: "https://researchr.org/alias/zolt%C3%A1n-horv%C3%A1th" - name: "Viktória Zsók" link: "https://researchr.org/alias/vikt%C3%B3ria-zs%C3%B3k" - name: "Peter Achten" link: "https://researchr.org/alias/peter-achten" - name: "Pieter W. M. Koopman" link: "https://researchr.org/alias/pieter-w.-m.-koopman" volume: "10" series: "Trends in Functional Programming" publisher: "Intellect" isbn: "978-1-84150-405-6" 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: "Mathematics of Program Construction - 12th International Conference, MPC 2015, Königswinter, Germany, June 29 - July 1, 2015. Proceedings" editor: - name: "Ralf Hinze" link: "https://researchr.org/alias/ralf-hinze" - name: "Janis Voigtländer" link: "https://researchr.org/alias/janis-voigtl%C3%A4nder" volume: "9129" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-19796-8" 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: "Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings" editor: - name: "Jacques Garrigue" link: "https://researchr.org/alias/jacques-garrigue" volume: "8858" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-12735-4" 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: "Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010" editor: - name: "Ekaterina Komendantskaya" link: "https://researchr.org/alias/ekaterina-komendantskaya" - name: "Ana Bove" link: "https://researchr.org/alias/ana-bove" - name: "Milad Niqui" link: "https://researchr.org/alias/milad-niqui" volume: "5" series: "EPiC Series" publisher: "EasyChair" kind: "inproceedings" key: "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: "Journal of Functional Programming" 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: "Practical Aspects of Declarative Languages - 15th International Symposium, PADL 2013, Rome, Italy, January 21-22, 2013. Proceedings" editor: - name: "Konstantinos F. Sagonas" link: "https://researchr.org/alias/konstantinos-f.-sagonas" volume: "7752" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-45283-3" 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 '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021" editor: - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "Andrei Popescu 0001" link: "https://researchr.org/alias/andrei-popescu-0001" publisher: "ACM" isbn: "978-1-4503-8299-1" 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: "Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009" editor: - name: "Thorsten Altenkirch" link: "http://www.cs.nott.ac.uk/~txa" - name: "Todd D. Millstein" link: "https://researchr.org/alias/todd-d.-millstein" publisher: "ACM" isbn: "978-1-60558-330-3" 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: "Implementation and Application of Functional Languages - 24th International Symposium, IFL 2012, Oxford, UK, August 30 - September 1, 2012, Revised Selected Papers" editor: - name: "Ralf Hinze" link: "https://researchr.org/alias/ralf-hinze" volume: "8241" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-41581-4" 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: "Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011" editor: - name: "Manuel M. T. Chakravarty" link: "https://researchr.org/alias/manuel-m.-t.-chakravarty" - name: "Zhenjiang Hu" link: "https://researchr.org/alias/zhenjiang-hu" - name: "Olivier Danvy" link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/" publisher: "ACM" isbn: "978-1-4503-0865-6" 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: "Electronic Notes in Theoretical Computer Science" 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: "Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008" editor: - name: "George C. Necula" link: "https://researchr.org/alias/george-c.-necula" - name: "Philip Wadler" link: "http://homepages.inf.ed.ac.uk/wadler/" publisher: "ACM" isbn: "978-1-59593-689-9" 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: "Journal of Functional Programming" 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: "28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013" publisher: "IEEE Computer Society" isbn: "978-1-4799-0413-6" 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: "Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings" editor: - name: "Stefan Berghofer" link: "https://researchr.org/alias/stefan-berghofer" - name: "Tobias Nipkow" link: "https://researchr.org/alias/tobias-nipkow" - name: "Christian Urban" link: "https://researchr.org/alias/christian-urban" - name: "Makarius Wenzel" link: "https://researchr.org/alias/makarius-wenzel" volume: "5674" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-03358-2" kind: "inproceedings" key: "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: "25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway" editor: - name: "Marc Bezem" link: "https://researchr.org/alias/marc-bezem" - name: "Assia Mahboubi" link: "https://researchr.org/alias/assia-mahboubi" volume: "175" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-158-0" kind: "inproceedings" key: "Cockx19" - title: "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: "Annals of Pure and Applied Logic" 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: "Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016" editor: - name: "Rastislav Bodik" link: "https://researchr.org/alias/rastislav-bodik" - name: "Rupak Majumdar" link: "https://researchr.org/alias/rupak-majumdar" publisher: "ACM" isbn: "978-1-4503-3549-2" 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: "Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings" editor: - name: "C.-H. Luke Ong" link: "https://researchr.org/alias/c.-h.-luke-ong" volume: "6014" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-12031-2" 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: "Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2018, St. Louis, MO, USA, September 27-17, 2018" editor: - name: "Nicolas Wu" link: "https://researchr.org/alias/nicolas-wu" publisher: "ACM" 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: "Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. P" editor: - name: "Martin Hofmann" link: "https://researchr.org/alias/martin-hofmann" volume: "6604" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-19804-5" 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: "Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017" editor: - name: "Yves Bertot" link: "https://researchr.org/alias/yves-bertot" - name: "Viktor Vafeiadis" link: "https://researchr.org/alias/viktor-vafeiadis" publisher: "ACM" isbn: "978-1-4503-4705-1" 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: "Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010" editor: - name: "Paul Hudak" link: "https://researchr.org/alias/paul-hudak" - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-60558-794-3" 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: "27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)" editor: - name: "Henning Basold" link: "https://researchr.org/alias/henning-basold" - name: "Jesper Cockx" link: "https://researchr.org/alias/jesper-cockx" - name: "Silvia Ghilezan" link: "https://researchr.org/alias/silvia-ghilezan" volume: "239" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-254-9" 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: "Journal of Functional Programming" 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: "Journal of Functional Programming" 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: "28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013" publisher: "IEEE Computer Society" isbn: "978-1-4799-0413-6" 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: "ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012" editor: - name: "Peter Thiemann" link: "https://researchr.org/alias/peter-thiemann" - name: "Robby Bruce Findler" link: "https://researchr.org/alias/robby-bruce-findler" publisher: "ACM" isbn: "978-1-4503-1054-3" kind: "inproceedings" key: "Danielsson12-0" - 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: "Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009" editor: - name: "Graham Hutton" link: "https://researchr.org/alias/graham-hutton" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" publisher: "ACM" isbn: "978-1-60558-332-7" 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: "Electronic Notes in Theoretical Computer Science" 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: "Proceedings of the ACM on Programming Languages" 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: "Implementation and Application of Functional Languages - 20th International Symposium, IFL 2008, Hatfield, UK, September 10-12, 2008. Revised Selected Papers" editor: - name: "Sven-Bodo Scholz" link: "https://researchr.org/alias/sven-bodo-scholz" - name: "Olaf Chitil" link: "https://researchr.org/alias/olaf-chitil" volume: "5836" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-24451-3" 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: "Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016" editor: - name: "Jacques Garrigue" link: "https://researchr.org/alias/jacques-garrigue" - name: "Gabriele Keller" link: "https://researchr.org/alias/gabriele-keller" - name: "Eijiro Sumii" link: "https://researchr.org/alias/eijiro-sumii" publisher: "ACM" isbn: "978-1-4503-4219-3" kind: "inproceedings" key: "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: "Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014" editor: - name: "Johan Jeuring" link: "https://researchr.org/alias/johan-jeuring" - name: "Manuel M. T. Chakravarty" link: "https://researchr.org/alias/manuel-m.-t.-chakravarty" publisher: "ACM" isbn: "978-1-4503-2873-9" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016" editor: - name: "Martin Grohe" link: "https://researchr.org/alias/martin-grohe" - name: "Eric Koskinen" link: "https://researchr.org/alias/eric-koskinen" - name: "Natarajan Shankar" link: "https://researchr.org/alias/natarajan-shankar" publisher: "ACM" isbn: "978-1-4503-4391-6" 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: "Proceedings of the sixth workshop on Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012" editor: - name: "Koen Claessen" link: "http://www.cse.chalmers.se/~koen/" - name: "Nikhil Swamy" link: "https://researchr.org/alias/nikhil-swamy" publisher: "ACM" isbn: "978-1-4503-1125-0" 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: "Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010" editor: - name: "Paul Hudak" link: "https://researchr.org/alias/paul-hudak" - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-60558-794-3" 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: "Proceedings of the ACM on Programming Languages" 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: "Trends in Functional Programming - 11th International Symposium, TFP 2010, Norman, OK, USA, May 17-19, 2010. Revised Selected Papers" editor: - name: "Rex L. Page" link: "https://researchr.org/alias/rex-l.-page" - name: "Zoltán Horváth" link: "https://researchr.org/alias/zolt%C3%A1n-horv%C3%A1th" - name: "Viktória Zsók" link: "https://researchr.org/alias/vikt%C3%B3ria-zs%C3%B3k" volume: "6546" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-22940-4" 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: "Proceedings of the ACM on Programming Languages" 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: "Electronic Notes in Theoretical Computer Science" 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: "The Seventeen Provers of the World, Foreword by Dana S. Scott" editor: - name: "Freek Wiedijk" link: "http://www.cs.ru.nl/~freek/" volume: "3600" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-30704-4" 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: "Implementation and Application of Functional Languages - 24th International Symposium, IFL 2012, Oxford, UK, August 30 - September 1, 2012, Revised Selected Papers" editor: - name: "Ralf Hinze" link: "https://researchr.org/alias/ralf-hinze" volume: "8241" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-41581-4" 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: "Proceedings of the 15th International Workshop on Logical and Semantic Frameworks with Applications, LSFA 2020, Online, September 15, 2019" editor: - name: "Cláudia Nalon" link: "https://researchr.org/alias/cl%C3%A1udia-nalon" volume: "351" series: "Electronic Notes in Theoretical Computer Science" publisher: "Elsevier" 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: "Journal of Functional Programming" 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: "Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009" editor: - name: "Thorsten Altenkirch" link: "http://www.cs.nott.ac.uk/~txa" - name: "Todd D. Millstein" link: "https://researchr.org/alias/todd-d.-millstein" publisher: "ACM" isbn: "978-1-60558-330-3" 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: "31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland" editor: - name: "Bartek Klin" link: "https://researchr.org/alias/bartek-klin" - name: "Elaine Pimentel" link: "https://researchr.org/alias/elaine-pimentel" volume: "252" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-264-8" 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: "Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2019, Berlin, Germany, August 18, 2019" editor: - name: "David Darais" link: "https://researchr.org/alias/david-darais" - name: "Jeremy Gibbons" link: "https://researchr.org/alias/jeremy-gibbons" publisher: "ACM" isbn: "978-1-4503-6815-5" 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: "Mathematical Structures in Computer Science" 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: "18th International Workshop on Types for Proofs and Programs, TYPES 2011, September 8-11, 2011, Bergen, Norway" editor: - name: "Nils Anders Danielsson" link: "https://researchr.org/alias/nils-anders-danielsson" - name: "Bengt Nordström" link: "https://researchr.org/alias/bengt-nordstr%C3%B6m" volume: "19" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-939897-49-1" 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: "Proceedings of the seventh ACM SIGPLAN workshop on Generic programming, WGP@ICFP 2011, Tokyo, Japan, September 19-21, 2011" editor: - name: "Jaakko Järvi" link: "https://researchr.org/alias/jaakko-j%C3%A4rvi" - name: "Shin-Cheng Mu" link: "https://researchr.org/alias/shin-cheng-mu" publisher: "ACM" isbn: "978-1-4503-0861-8" 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: "Logical Foundations of Computer Science - International Symposium, LFCS 2016, Deerfield Beach, FL, USA, January 4-7, 2016. Proceedings" editor: - name: "Sergei N. Artëmov" link: "https://researchr.org/alias/sergei-n.-art%C3%ABmov" - name: "Anil Nerode" link: "https://researchr.org/alias/anil-nerode" volume: "9537" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-27682-3" 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: "Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008" editor: - name: "George C. Necula" link: "https://researchr.org/alias/george-c.-necula" - name: "Philip Wadler" link: "http://homepages.inf.ed.ac.uk/wadler/" publisher: "ACM" isbn: "978-1-59593-689-9" 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: "Electronic Notes in Theoretical Computer Science" 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: "Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011" editor: - name: "Manuel M. T. Chakravarty" link: "https://researchr.org/alias/manuel-m.-t.-chakravarty" - name: "Zhenjiang Hu" link: "https://researchr.org/alias/zhenjiang-hu" - name: "Olivier Danvy" link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/" publisher: "ACM" isbn: "978-1-4503-0865-6" 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: "Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014" editor: - name: "Olaf Chitil" link: "https://researchr.org/alias/olaf-chitil" - name: "Andy King" link: "https://researchr.org/alias/andy-king" - name: "Olivier Danvy" link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/" publisher: "ACM" isbn: "978-1-4503-2947-7" kind: "inproceedings" key: "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: "Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, WGP@ICFP 2015, Vancouver, BC, Canada, August 30, 2015" editor: - name: "Patrick Bahr" link: "https://researchr.org/alias/patrick-bahr" - name: "Sebastian Erdweg" link: "http://www.informatik.uni-marburg.de/~seba/" publisher: "ACM" isbn: "978-1-4503-3810-3" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020" editor: - name: "Jasmin Blanchette" link: "https://researchr.org/alias/jasmin-blanchette" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" publisher: "ACM" isbn: "978-1-4503-7097-4" 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: "Science of Computer Programming" 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: "Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017" editor: - name: "Giuseppe Castagna" link: "https://researchr.org/alias/giuseppe-castagna" - name: "Andrew D. Gordon" link: "https://researchr.org/alias/andrew-d.-gordon" publisher: "ACM" isbn: "978-1-4503-4660-3" kind: "inproceedings" key: "OmarVHAH17" - 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: "Mathematics of Program Construction - 12th International Conference, MPC 2015, Königswinter, Germany, June 29 - July 1, 2015. Proceedings" editor: - name: "Ralf Hinze" link: "https://researchr.org/alias/ralf-hinze" - name: "Janis Voigtländer" link: "https://researchr.org/alias/janis-voigtl%C3%A4nder" volume: "9129" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-19796-8" 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 '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022" editor: - name: "Andrei Popescu 0001" link: "https://researchr.org/alias/andrei-popescu-0001" - name: "Steve Zdancewic" link: "https://researchr.org/alias/steve-zdancewic" publisher: "ACM" isbn: "978-1-4503-9182-5" kind: "inproceedings" key: "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: "13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland" editor: - name: "Thorsten Altenkirch" link: "https://researchr.org/alias/thorsten-altenkirch" volume: "38" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-939897-87-3" kind: "inproceedings" key: "EscardoX15" - 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: "Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings" editor: - name: "John P. Gallagher" link: "https://researchr.org/alias/john-p.-gallagher" - name: "Martin Sulzmann" link: "https://researchr.org/alias/martin-sulzmann" volume: "10818" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-90686-7" 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: "Proceedings of the Nineth Symposium on Trends in Functional Programming, TFP 2008, Nijmegen, The Netherlands, May 26-28, 2008" editor: - name: "Peter Achten" link: "https://researchr.org/alias/peter-achten" - name: "Pieter W. M. Koopman" link: "https://researchr.org/alias/pieter-w.-m.-koopman" - name: "Marco T. Morazán" link: "https://researchr.org/alias/marco-t.-moraz%C3%A1n" volume: "9" series: "Trends in Functional Programming" publisher: "Intellect" isbn: "978-1-84150-277-9" 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: "Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings" editor: - name: "Lars Birkedal" link: "https://researchr.org/alias/lars-birkedal" volume: "7213" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-28728-2" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, MSFP@ICFP 2010, Baltimore, MD, USA, September 25, 2010" editor: - name: "Venanzio Capretta" link: "https://researchr.org/alias/venanzio-capretta" - name: "James Chapman 0001" link: "https://researchr.org/alias/james-chapman-0001" publisher: "ACM" isbn: "978-1-4503-0255-5" 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: "Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020" editor: - name: "Jasmin Blanchette" link: "https://researchr.org/alias/jasmin-blanchette" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" publisher: "ACM" isbn: "978-1-4503-7097-4" 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: "Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2019, Berlin, Germany, August 18, 2019" editor: - name: "David Darais" link: "https://researchr.org/alias/david-darais" - name: "Jeremy Gibbons" link: "https://researchr.org/alias/jeremy-gibbons" publisher: "ACM" isbn: "978-1-4503-6815-5" 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: "Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2019, Berlin, Germany, August 18, 2019" editor: - name: "David Darais" link: "https://researchr.org/alias/david-darais" - name: "Jeremy Gibbons" link: "https://researchr.org/alias/jeremy-gibbons" publisher: "ACM" isbn: "978-1-4503-6815-5" kind: "inproceedings" key: "OConnor19" - 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: "Journal of Functional Programming" 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: "Logical Foundations of Computer Science - International Symposium, LFCS 2016, Deerfield Beach, FL, USA, January 4-7, 2016. Proceedings" editor: - name: "Sergei N. Artëmov" link: "https://researchr.org/alias/sergei-n.-art%C3%ABmov" - name: "Anil Nerode" link: "https://researchr.org/alias/anil-nerode" volume: "9537" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-27682-3" 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: "Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings" editor: - name: "Jeremy Avigad" link: "https://researchr.org/alias/jeremy-avigad" - name: "Assia Mahboubi" link: "https://researchr.org/alias/assia-mahboubi" volume: "10895" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-94821-8" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceedings of the seventh ACM SIGPLAN workshop on Generic programming, WGP@ICFP 2011, Tokyo, Japan, September 19-21, 2011" editor: - name: "Jaakko Järvi" link: "https://researchr.org/alias/jaakko-j%C3%A4rvi" - name: "Shin-Cheng Mu" link: "https://researchr.org/alias/shin-cheng-mu" publisher: "ACM" isbn: "978-1-4503-0861-8" 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: "Proceedings of the ACM on Programming Languages" 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: "Relational and Algebraic Methods in Computer Science - 15th International Conference, RAMiCS 2015, Braga, Portugal, September 28 - October 1, 2015, Proceedings" editor: - name: "Wolfram Kahl" link: "https://researchr.org/alias/wolfram-kahl" - name: "Michael Winter" link: "https://researchr.org/alias/michael-winter" - name: "José N. Oliveira" link: "https://researchr.org/alias/jos%C3%A9-n.-oliveira" volume: "9348" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-24703-8" 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: "Annals of Pure and Applied Logic" 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: "Proceedings of the seventh ACM SIGPLAN workshop on Generic programming, WGP@ICFP 2011, Tokyo, Japan, September 19-21, 2011" editor: - name: "Jaakko Järvi" link: "https://researchr.org/alias/jaakko-j%C3%A4rvi" - name: "Shin-Cheng Mu" link: "https://researchr.org/alias/shin-cheng-mu" publisher: "ACM" isbn: "978-1-4503-0861-8" 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: "Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings" editor: - name: "Herman Geuvers" link: "https://researchr.org/alias/herman-geuvers" - name: "Matthew England" link: "https://researchr.org/alias/matthew-england" - name: "Osman Hasan" link: "https://researchr.org/alias/osman-hasan" - name: "Florian Rabe" link: "https://researchr.org/alias/florian-rabe" - name: "Olaf Teschke" link: "https://researchr.org/alias/olaf-teschke" volume: "10383" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-62075-6" 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 for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers" editor: - name: "Jean-Christophe Filliâtre" link: "https://researchr.org/alias/jean-christophe-filli%C3%A2tre" - name: "Christine Paulin-Mohring" link: "https://researchr.org/alias/christine-paulin-mohring" - name: "Benjamin Werner" link: "https://researchr.org/alias/benjamin-werner" volume: "3839" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-31428-8" 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: "Journal of Functional Programming" 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: "Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010" editor: - name: "Paul Hudak" link: "https://researchr.org/alias/paul-hudak" - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-60558-794-3" 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: "ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013" editor: - name: "Greg Morrisett" link: "https://researchr.org/alias/greg-morrisett" - name: "Tarmo Uustalu" link: "https://researchr.org/alias/tarmo-uustalu" publisher: "ACM" isbn: "978-1-4503-2326-0" 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: "30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015" publisher: "IEEE" isbn: "978-1-4799-8875-4" 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: "23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary" editor: - name: "Andreas Abel 0001" link: "https://researchr.org/alias/andreas-abel-0001" - name: "Fredrik Nordvall Forsberg" link: "https://researchr.org/alias/fredrik-nordvall-forsberg" - name: "Ambrus Kaposi" link: "https://researchr.org/alias/ambrus-kaposi" volume: "104" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-95977-071-2" 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: "Journal of Symbolic Logic" 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: "Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014" editor: - name: "Thomas A. Henzinger" link: "https://researchr.org/alias/thomas-a.-henzinger" - name: "Dale Miller" link: "https://researchr.org/alias/dale-miller" publisher: "ACM" isbn: "978-1-4503-2886-9" 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: "CLEI Electron. J." 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: "Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, DTP@ICFP 2013, Boston, Massachusetts, USA, September 24, 2013" editor: - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-4503-2384-0" 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: "Proceedings of the 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013" editor: - name: "Matthew Might" link: "https://researchr.org/alias/matthew-might" - name: "David Van Horn" link: "https://researchr.org/alias/david-van-horn" - name: "Andreas Abel 0001" link: "https://researchr.org/alias/andreas-abel-0001" - name: "Tim Sheard" link: "https://researchr.org/alias/tim-sheard" publisher: "ACM" isbn: "978-1-4503-1860-0" 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: "Functional and Constraint Logic Programming - 26th International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers" editor: - name: "Josep Silva" link: "https://researchr.org/alias/josep-silva" volume: "11285" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-030-16202-3" 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: "Journal of Automated Reasoning" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014" editor: - name: "Johan Jeuring" link: "https://researchr.org/alias/johan-jeuring" - name: "Manuel M. T. Chakravarty" link: "https://researchr.org/alias/manuel-m.-t.-chakravarty" publisher: "ACM" isbn: "978-1-4503-2873-9" 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: "Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011" editor: - name: "Manuel M. T. Chakravarty" link: "https://researchr.org/alias/manuel-m.-t.-chakravarty" - name: "Zhenjiang Hu" link: "https://researchr.org/alias/zhenjiang-hu" - name: "Olivier Danvy" link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/" publisher: "ACM" isbn: "978-1-4503-0865-6" 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: "Proceedings of the ACM on Programming Languages" 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: "Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings" editor: - name: "Gilles Dowek" link: "https://researchr.org/alias/gilles-dowek" volume: "8560" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-08917-1" kind: "inproceedings" key: "Setzer0PT14" - title: "MiniAgda: Integrating Sized and Dependent Types" author: - name: "Andreas Abel" link: "http://www.cse.chalmers.se/~abela/" year: "2010" doi: "http://www.easychair.org/publications/?page=506004245" links: doi: "http://www.easychair.org/publications/?page=506004245" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/000110" researchr: "https://researchr.org/publication/000110-2" cites: 0 citedby: 0 pages: "18-32" booktitle: "Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010" editor: - name: "Ekaterina Komendantskaya" link: "https://researchr.org/alias/ekaterina-komendantskaya" - name: "Ana Bove" link: "https://researchr.org/alias/ana-bove" - name: "Milad Niqui" link: "https://researchr.org/alias/milad-niqui" volume: "5" series: "EPiC Series" publisher: "EasyChair" kind: "inproceedings" key: "000110-2" - title: "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: "Proceedings of the ACM on Programming Languages" 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: "Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings" editor: - name: "Philippe Audebaud" link: "https://researchr.org/alias/philippe-audebaud" - name: "Christine Paulin-Mohring" link: "https://researchr.org/alias/christine-paulin-mohring" volume: "5133" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-70593-2" 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: "Journal of Functional Programming" 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: "Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings" editor: - name: "Masahito Hasegawa" link: "https://researchr.org/alias/masahito-hasegawa" volume: "7941" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-38946-7" 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: "NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings" editor: - name: "Jyotirmoy V. Deshmukh" link: "https://researchr.org/alias/jyotirmoy-v.-deshmukh" - name: "Klaus Havelund" link: "https://researchr.org/alias/klaus-havelund" - name: "Ivan Perez 0001" link: "https://researchr.org/alias/ivan-perez-0001" volume: "13260" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-031-06773-0" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015" editor: - name: "Xavier Leroy" link: "http://pauillac.inria.fr/~xleroy/" - name: "Alwen Tiu" link: "https://researchr.org/alias/alwen-tiu" publisher: "ACM" isbn: "978-1-4503-3296-5" 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: "Proceedings of the ACM on Programming Languages" 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: "Journal of Functional Programming" 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: "Relational and Algebraic Methods in Computer Science - 12th International Conference, RAMICS 2011, Rotterdam, The Netherlands, May 30 - June 3, 2011. Proceedings" editor: - name: "Harrie C. M. de Swart" link: "https://researchr.org/alias/harrie-c.-m.-de-swart" volume: "6663" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-21069-3" 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: "Proceedings of the ACM on Programming Languages" 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: "Theoretical Computer Science" 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: "Proceedings of the seventh ACM SIGPLAN workshop on Generic programming, WGP@ICFP 2011, Tokyo, Japan, September 19-21, 2011" editor: - name: "Jaakko Järvi" link: "https://researchr.org/alias/jaakko-j%C3%A4rvi" - name: "Shin-Cheng Mu" link: "https://researchr.org/alias/shin-cheng-mu" publisher: "ACM" isbn: "978-1-4503-0861-8" 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: "Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, DTP@ICFP 2013, Boston, Massachusetts, USA, September 24, 2013" editor: - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-4503-2384-0" 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: "Higher-Order and Symbolic Computation" 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: "Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010" editor: - name: "Ekaterina Komendantskaya" link: "https://researchr.org/alias/ekaterina-komendantskaya" - name: "Ana Bove" link: "https://researchr.org/alias/ana-bove" - name: "Milad Niqui" link: "https://researchr.org/alias/milad-niqui" volume: "5" series: "EPiC Series" publisher: "EasyChair" kind: "inproceedings" key: "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: "Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings" editor: - name: "Kirstin Peters" link: "https://researchr.org/alias/kirstin-peters" - name: "Tim A. C. Willemse" link: "https://researchr.org/alias/tim-a.-c.-willemse" volume: "12719" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-030-78089-0" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010" editor: - name: "Paul Hudak" link: "https://researchr.org/alias/paul-hudak" - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-60558-794-3" 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: "Annals of Pure and Applied Logic" 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: "Proceedings of the ACM on Programming Languages" 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: "ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013" editor: - name: "Greg Morrisett" link: "https://researchr.org/alias/greg-morrisett" - name: "Tarmo Uustalu" link: "https://researchr.org/alias/tarmo-uustalu" publisher: "ACM" isbn: "978-1-4503-2326-0" kind: "inproceedings" key: "DevrieseP13" - 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: "Proceedings of the ACM on Programming Languages" 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: "Proceedings of the ACM on Programming Languages" 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: "NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings" editor: - name: "Mihaela Gheorghiu Bobaru" link: "https://researchr.org/alias/mihaela-gheorghiu-bobaru" - name: "Klaus Havelund" link: "https://researchr.org/alias/klaus-havelund" - name: "Gerard J. Holzmann" link: "https://researchr.org/alias/gerard-j.-holzmann" - name: "Rajeev Joshi" link: "https://researchr.org/alias/rajeev-joshi" volume: "6617" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-20397-8" 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: "21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia" editor: - name: "Tarmo Uustalu" link: "https://researchr.org/alias/tarmo-uustalu" volume: "69" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-95977-030-9" 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" note: "base-search.net (ftunivleuven:oai:lirias.kuleuven.be:123456789/583556)" 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 '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022" editor: - name: "Andrei Popescu 0001" link: "https://researchr.org/alias/andrei-popescu-0001" - name: "Steve Zdancewic" link: "https://researchr.org/alias/steve-zdancewic" publisher: "ACM" isbn: "978-1-4503-9182-5" kind: "inproceedings" key: "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: "Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010" editor: - name: "Ekaterina Komendantskaya" link: "https://researchr.org/alias/ekaterina-komendantskaya" - name: "Ana Bove" link: "https://researchr.org/alias/ana-bove" - name: "Milad Niqui" link: "https://researchr.org/alias/milad-niqui" volume: "5" series: "EPiC Series" publisher: "EasyChair" kind: "inproceedings" key: "AltenkirchD10" - 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: "Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings" editor: - name: "Peter Thiemann" link: "https://researchr.org/alias/peter-thiemann" volume: "9632" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-662-49497-4" 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 '21: Concepts and Experiences, Chicago, IL, USA, October 17 - 18, 2021" editor: - name: "Eli Tilevich" link: "https://researchr.org/alias/eli-tilevich" - name: "Coen De Roover" link: "https://researchr.org/alias/coen-de-roover" publisher: "ACM" isbn: "978-1-4503-9112-2" 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: "Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings" editor: - name: "Masahito Hasegawa" link: "https://researchr.org/alias/masahito-hasegawa" volume: "7941" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-38946-7" 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: "Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017" editor: - name: "Yves Bertot" link: "https://researchr.org/alias/yves-bertot" - name: "Viktor Vafeiadis" link: "https://researchr.org/alias/viktor-vafeiadis" publisher: "ACM" isbn: "978-1-4503-4705-1" 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: "Journal of Logic and Algebraic Programming" 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: "Journal of Functional Programming" 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" address: "New York, NY, USA" publisher: "ACM" isbn: "978-1-60558-510-9" 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: "Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2018, St. Louis, MO, USA, September 27, 2018" editor: - name: "Richard A. Eisenberg" link: "https://researchr.org/alias/richard-a.-eisenberg" - name: "Niki Vazou" link: "https://researchr.org/alias/niki-vazou" publisher: "ACM" 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: "Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014" editor: - name: "Johan Jeuring" link: "https://researchr.org/alias/johan-jeuring" - name: "Manuel M. T. Chakravarty" link: "https://researchr.org/alias/manuel-m.-t.-chakravarty" publisher: "ACM" isbn: "978-1-4503-2873-9" 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: "Proceedings of the ACM on Programming Languages" 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: "Electronic Notes in Theoretical Computer Science" 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: "Journal of Logic and Algebraic Programming" 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: "Electronic Notes in Theoretical Computer Science" 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: "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: "Journal of Functional Programming" 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: "Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings" editor: - name: "Lars Birkedal" link: "https://researchr.org/alias/lars-birkedal" volume: "7213" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-28728-2" 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: "Proceedings of the 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013" editor: - name: "Matthew Might" link: "https://researchr.org/alias/matthew-might" - name: "David Van Horn" link: "https://researchr.org/alias/david-van-horn" - name: "Andreas Abel 0001" link: "https://researchr.org/alias/andreas-abel-0001" - name: "Tim Sheard" link: "https://researchr.org/alias/tim-sheard" publisher: "ACM" isbn: "978-1-4503-1860-0" 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: "30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference)" editor: - name: "Florin Manea" link: "https://researchr.org/alias/florin-manea" - name: "Alex Simpson" link: "https://researchr.org/alias/alex-simpson" volume: "216" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-218-1" 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: "5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference)" editor: - name: "Zena M. Ariola" link: "https://researchr.org/alias/zena-m.-ariola" volume: "167" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-155-9" kind: "inproceedings" key: "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: "Journal of Functional Programming" 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: "Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014" editor: - name: "Johan Jeuring" link: "https://researchr.org/alias/johan-jeuring" - name: "Manuel M. T. Chakravarty" link: "https://researchr.org/alias/manuel-m.-t.-chakravarty" publisher: "ACM" isbn: "978-1-4503-2873-9" 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: "Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020" editor: - name: "Jasmin Blanchette" link: "https://researchr.org/alias/jasmin-blanchette" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" publisher: "ACM" isbn: "978-1-4503-7097-4" 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: "Journal of Functional Programming" 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: "Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, DTP@ICFP 2013, Boston, Massachusetts, USA, September 24, 2013" editor: - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-4503-2384-0" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009" editor: - name: "Graham Hutton" link: "https://researchr.org/alias/graham-hutton" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" publisher: "ACM" isbn: "978-1-60558-332-7" kind: "inproceedings" key: "LicataH09" - 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: "J. Formalized Reasoning" 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: "Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, MSFP@ICFP 2010, Baltimore, MD, USA, September 25, 2010" editor: - name: "Venanzio Capretta" link: "https://researchr.org/alias/venanzio-capretta" - name: "James Chapman 0001" link: "https://researchr.org/alias/james-chapman-0001" publisher: "ACM" isbn: "978-1-4503-0255-5" 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: "Programming Languages - 18th Brazilian Symposium, SBLP 2014, Maceio, Brazil, October 2-3, 2014. Proceedings" editor: - name: "Fernando Magno Quintão Pereira" link: "https://researchr.org/alias/fernando-magno-quint%C3%A3o-pereira" volume: "8771" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-11862-8" 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: "Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings" editor: - name: "Anuj Dawar" link: "https://researchr.org/alias/anuj-dawar" - name: "Helmut Veith" link: "https://researchr.org/alias/helmut-veith" volume: "6247" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-15204-7" kind: "inproceedings" key: "ForsbergS10" - 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: "Formal Methods: Foundations and Applications - 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26-30, 2018, Proceedings" editor: - name: "Tiago Massoni" link: "https://researchr.org/alias/tiago-massoni" - name: "Mohammad Reza Mousavi" link: "https://researchr.org/alias/mohammad-reza-mousavi" volume: "11254" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-030-03044-5" 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: "Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017" editor: - name: "Wim Vanhoof" link: "https://researchr.org/alias/wim-vanhoof" - name: "Brigitte Pientka" link: "https://researchr.org/alias/brigitte-pientka" publisher: "ACM" isbn: "978-1-4503-5291-8" 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: "Electronic Notes in Theoretical Computer Science" 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: "Proceedings of the ACM on Programming Languages" 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: "ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, Edinburgh, United Kingdom - June 09 - 11, 2014" editor: - name: "Michael F. P. O'Boyle" link: "https://researchr.org/alias/michael-f.-p.-o%27boyle" - name: "Keshav Pingali" link: "https://researchr.org/alias/keshav-pingali" publisher: "ACM" isbn: "978-1-4503-2784-8" 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: "Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings" editor: - name: "Masahito Hasegawa" link: "https://researchr.org/alias/masahito-hasegawa" volume: "7941" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-38946-7" 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" note: "British Library, EThOS" 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: "27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)" editor: - name: "Henning Basold" link: "https://researchr.org/alias/henning-basold" - name: "Jesper Cockx" link: "https://researchr.org/alias/jesper-cockx" - name: "Silvia Ghilezan" link: "https://researchr.org/alias/silvia-ghilezan" volume: "239" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-254-9" 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: "Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007" editor: - name: "Aaron Stump" link: "https://researchr.org/alias/aaron-stump" - name: "Hongwei Xi" link: "http://www.cs.bu.edu/~hwxi/" publisher: "ACM" isbn: "978-1-59593-677-6" 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: "Implementation and Application of Functional Languages - 24th International Symposium, IFL 2012, Oxford, UK, August 30 - September 1, 2012, Revised Selected Papers" editor: - name: "Ralf Hinze" link: "https://researchr.org/alias/ralf-hinze" volume: "8241" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-41581-4" 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: "27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)" editor: - name: "Henning Basold" link: "https://researchr.org/alias/henning-basold" - name: "Jesper Cockx" link: "https://researchr.org/alias/jesper-cockx" - name: "Silvia Ghilezan" link: "https://researchr.org/alias/silvia-ghilezan" volume: "239" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-254-9" 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 for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers" editor: - name: "Thorsten Altenkirch" link: "http://www.cs.nott.ac.uk/~txa" - name: "Conor McBride" link: "https://researchr.org/alias/conor-mcbride" volume: "4502" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-74463-4" kind: "inproceedings" key: "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: "Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings" editor: - name: "Bor-Yuh Evan Chang" link: "https://researchr.org/alias/bor-yuh-evan-chang" volume: "10695" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-71237-6" 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: "Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, SIGCOMM 2018, Budapest, Hungary, August 20-25, 2018" editor: - name: "Sergey Gorinsky" link: "https://researchr.org/alias/sergey-gorinsky" - name: "János Tapolcai" link: "https://researchr.org/alias/j%C3%A1nos-tapolcai" publisher: "ACM" 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: "Proceedings of the 1st International Workshop on Type-Driven Development, TyDe@ICFP 2016, Nara, Japan, September 18, 2016" editor: - name: "James Chapman" link: "https://researchr.org/alias/james-chapman" - name: "Wouter Swierstra" link: "https://researchr.org/alias/wouter-swierstra" publisher: "ACM" isbn: "978-1-4503-4435-7" 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: "ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012" editor: - name: "Peter Thiemann" link: "https://researchr.org/alias/peter-thiemann" - name: "Robby Bruce Findler" link: "https://researchr.org/alias/robby-bruce-findler" publisher: "ACM" isbn: "978-1-4503-1054-3" 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: "ACM Trans. Comput. Log." 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: "Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014" editor: - name: "Thomas A. Henzinger" link: "https://researchr.org/alias/thomas-a.-henzinger" - name: "Dale Miller" link: "https://researchr.org/alias/dale-miller" publisher: "ACM" isbn: "978-1-4503-2886-9" 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: "Proceedings of the 10th ACM SIGPLAN workshop on Generic programming, WGP 2014, Gothenburg, Sweden, August 31, 2014" editor: - name: "José Pedro Magalháes" link: "https://researchr.org/alias/jos%C3%A9-pedro-magalh%C3%A1es" - name: "Tiark Rompf" link: "https://researchr.org/alias/tiark-rompf" publisher: "ACM" isbn: "978-1-4503-3042-8" 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: "J. Formalized Reasoning" 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: "Theoretical Aspects of Computing - ICTAC 2017 - 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings" editor: - name: "Dang Van Hung" link: "https://researchr.org/alias/dang-van-hung" - name: "Deepak Kapur" link: "https://researchr.org/alias/deepak-kapur" volume: "10580" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-67729-3" 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: "13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland" editor: - name: "Thorsten Altenkirch" link: "https://researchr.org/alias/thorsten-altenkirch" volume: "38" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-939897-87-3" 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: "Proceedings of the 15th International Workshop on Logical and Semantic Frameworks with Applications, LSFA 2020, Online, September 15, 2019" editor: - name: "Cláudia Nalon" link: "https://researchr.org/alias/cl%C3%A1udia-nalon" volume: "351" series: "Electronic Notes in Theoretical Computer Science" publisher: "Elsevier" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008" editor: - name: "James Hook" link: "https://researchr.org/alias/james-hook" - name: "Peter Thiemann" link: "http://www.informatik.uni-freiburg.de/~thiemann/" publisher: "ACM" isbn: "978-1-59593-919-7" 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: "Proceedings of the ACM on Programming Languages" 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: "Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings" editor: - name: "Georges Gonthier" link: "https://researchr.org/alias/georges-gonthier" - name: "Michael Norrish" link: "https://researchr.org/alias/michael-norrish" volume: "8307" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-03544-4" 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: "Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings" editor: - name: "Zhong Shao" link: "https://researchr.org/alias/zhong-shao" volume: "8410" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-54832-1" 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: "Proceedings of the ACM on Programming Languages" volume: "3" kind: "article" key: "VassenaRGRS19" - 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: "Proceedings of the 24th International Workshop on Description Logics (DL 2011), Barcelona, Spain, July 13-16, 2011" editor: - name: "Riccardo Rosati" link: "https://researchr.org/alias/riccardo-rosati" - name: "Sebastian Rudolph" link: "https://researchr.org/alias/sebastian-rudolph" - name: "Michael Zakharyaschev" link: "https://researchr.org/alias/michael-zakharyaschev" volume: "745" series: "CEUR Workshop Proceedings" publisher: "CEUR-WS.org" 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: "Proceedings of the ACM on Programming Languages" 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: "24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany" editor: - name: "Stephan Kreutzer" link: "https://researchr.org/alias/stephan-kreutzer" volume: "41" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-939897-90-3" 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" note: "British Library, EThOS" 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: "Journal of Functional Programming" 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: "ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012" editor: - name: "Peter Thiemann" link: "https://researchr.org/alias/peter-thiemann" - name: "Robby Bruce Findler" link: "https://researchr.org/alias/robby-bruce-findler" publisher: "ACM" isbn: "978-1-4503-1054-3" 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: "Proceedings of TLDI 08: 2008 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009" editor: - name: "Andrew Kennedy" link: "https://researchr.org/alias/andrew-kennedy" - name: "Amal Ahmed" link: "https://researchr.org/alias/amal-ahmed" publisher: "ACM" isbn: "978-1-60558-420-1" 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: "Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings" editor: - name: "Andrew M. Pitts" link: "https://researchr.org/alias/andrew-m.-pitts" volume: "9034" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-662-46677-3" 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: "Relational and Algebraic Methods in Computer Science - 13th International Conference, RAMiCS 2012, Cambridge, UK, September 17-20, 2012. Proceedings" editor: - name: "Wolfram Kahl" link: "https://researchr.org/alias/wolfram-kahl" - name: "Timothy G. Griffin" link: "https://researchr.org/alias/timothy-g.-griffin" volume: "7560" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-33313-2" 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: "22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia" editor: - name: "Silvia Ghilezan" link: "https://researchr.org/alias/silvia-ghilezan" - name: "Herman Geuvers" link: "https://researchr.org/alias/herman-geuvers" - name: "Jelena Ivetic" link: "https://researchr.org/alias/jelena-ivetic" volume: "97" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-95977-065-1" kind: "inproceedings" key: "IgriedS16-0" - 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: "12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)" editor: - name: "Liron Cohen 0001" link: "https://researchr.org/alias/liron-cohen-0001" - name: "Cezary Kaliszyk" link: "https://researchr.org/alias/cezary-kaliszyk" volume: "193" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-188-7" kind: "inproceedings" key: "CicconeDZ21" - 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: "Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings" editor: - name: "Reiko Heckel" link: "https://researchr.org/alias/reiko-heckel" - name: "Stefan Milius" link: "https://researchr.org/alias/stefan-milius" volume: "8089" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-40205-0" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2019, Cascais, Portugal, January 14-15, 2019" editor: - name: "Manuel V. Hermenegildo" link: "https://researchr.org/alias/manuel-v.-hermenegildo" - name: "Atsushi Igarashi" link: "https://researchr.org/alias/atsushi-igarashi" publisher: "ACM" isbn: "978-1-4503-6226-9" 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: "Proceedings of the ACM SIGPLAN Workshop on Generic Programming, WGP 2010, Baltimore, MD, USA, September 27-29, 2010" editor: - name: "Bruno C. d. S. Oliveira" link: "http://ropas.snu.ac.kr/~bruno/" - name: "Marcin Zalewski" link: "http://www.google.com" publisher: "ACM" isbn: "978-1-4503-0251-7" 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: "Proceedings of the ACM on Programming Languages" 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: "Logical Methods in Computer Science" 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: "Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS@CCS 2016, Vienna, Austria, October 24, 2016" editor: - name: "Toby C. Murray" link: "https://researchr.org/alias/toby-c.-murray" - name: "Deian Stefan" link: "https://researchr.org/alias/deian-stefan" publisher: "ACM" isbn: "978-1-4503-4574-3" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2020, Virtual Event, USA, August 23, 2020" editor: - name: "James McKinna" link: "https://researchr.org/alias/james-mckinna" - name: "Cyrus Omar" link: "https://researchr.org/alias/cyrus-omar" publisher: "ACM" isbn: "978-1-4503-8051-5" kind: "inproceedings" key: "JuanD20" - title: "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 '22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15 - 16, 2022" editor: - name: "Nadia Polikarpova" link: "https://researchr.org/alias/nadia-polikarpova" publisher: "ACM" isbn: "978-1-4503-9438-3" 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: "Proceedings of the 14th Symposium on Programming Languages and Software Tools (SPLST'15), Tampere, Finland, October 9-10, 2015" editor: - name: "Jyrki Nummenmaa" link: "https://researchr.org/alias/jyrki-nummenmaa" - name: "Outi Sievi-Korte" link: "https://researchr.org/alias/outi-sievi-korte" - name: "Erkki Mäkinen" link: "https://researchr.org/alias/erkki-m%C3%A4kinen" volume: "1525" series: "CEUR Workshop Proceedings" publisher: "CEUR-WS.org" 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: "1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal" editor: - name: "Delia Kesner" link: "https://researchr.org/alias/delia-kesner" - name: "Brigitte Pientka" link: "https://researchr.org/alias/brigitte-pientka" volume: "52" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-95977-010-1" 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: "Journal of Functional Programming" 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: "4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany" editor: - name: "Herman Geuvers" link: "https://researchr.org/alias/herman-geuvers" volume: "131" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-95977-107-8" 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: "Mathematical Structures in Computer Science" 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: "28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013" publisher: "IEEE Computer Society" isbn: "978-1-4799-0413-6" 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: "Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014" editor: - name: "Amy P. Felty" link: "https://researchr.org/alias/amy-p.-felty" - name: "Brigitte Pientka" link: "https://researchr.org/alias/brigitte-pientka" publisher: "ACM" isbn: "978-1-4503-2817-3" 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: "Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings" editor: - name: "Martin Leucker" link: "https://researchr.org/alias/martin-leucker" - name: "Camilo Rueda" link: "https://researchr.org/alias/camilo-rueda" - name: "Frank D. Valencia" link: "https://researchr.org/alias/frank-d.-valencia" volume: "9399" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-25149-3" 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: "Proceedings of the 1st International Workshop on Type-Driven Development, TyDe@ICFP 2016, Nara, Japan, September 18, 2016" editor: - name: "James Chapman" link: "https://researchr.org/alias/james-chapman" - name: "Wouter Swierstra" link: "https://researchr.org/alias/wouter-swierstra" publisher: "ACM" isbn: "978-1-4503-4435-7" 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: "Proceedings of the ACM on Programming Languages" 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: "Proceedings of the ACM on Programming Languages" 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 '20: 24th Brazilian Symposium on Programming Languages, Natal, Rio Grande do Norte, Brazil, October 19-23, 2020" editor: - name: "Everton Cavalcante" link: "https://researchr.org/alias/everton-cavalcante" - name: "Francisco Dantas" link: "https://researchr.org/alias/francisco-dantas" - name: "Thaís Batista" link: "https://researchr.org/alias/tha%C3%ADs-batista" publisher: "ACM" isbn: "978-1-4503-8943-3" 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: "NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings" editor: - name: "Aaron Dutle" link: "https://researchr.org/alias/aaron-dutle" - name: "César A. Muñoz" link: "https://researchr.org/alias/c%C3%A9sar-a.-mu%C3%B1oz" - name: "Anthony Narkawicz" link: "https://researchr.org/alias/anthony-narkawicz" volume: "10811" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-77935-5" 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: "Journal of Functional Programming" 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: "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: "Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings" editor: - name: "Lennart Beringer" link: "https://researchr.org/alias/lennart-beringer" - name: "Amy P. Felty" link: "https://researchr.org/alias/amy-p.-felty" volume: "7406" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-32346-1" kind: "inproceedings" key: "Danielsson12" - 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: "Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, DTP@ICFP 2013, Boston, Massachusetts, USA, September 24, 2013" editor: - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-4503-2384-0" 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: "Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings" editor: - name: "Graham Hutton" link: "https://researchr.org/alias/graham-hutton" volume: "11825" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-030-33636-3" 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: "Proceedings of the ACM on Programming Languages" 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: "23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary" editor: - name: "Andreas Abel 0001" link: "https://researchr.org/alias/andreas-abel-0001" - name: "Fredrik Nordvall Forsberg" link: "https://researchr.org/alias/fredrik-nordvall-forsberg" - name: "Ambrus Kaposi" link: "https://researchr.org/alias/ambrus-kaposi" volume: "104" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-95977-071-2" kind: "inproceedings" key: "Allais17"