% Bibliography downloaded from https://researchr.org/downloadbibtex/bibliography/agda-papers

@inproceedings{AltenkirchDK17,
  title = {Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type},
  author = {Thorsten Altenkirch and Nils Anders Danielsson and Nicolai Kraus},
  year = {2017},
  doi = {10.1007/978-3-662-54458-7_31},
  url = {http://dx.doi.org/10.1007/978-3-662-54458-7_31},
  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 = {Javier Esparza and Andrzej S. Murawski},
  volume = {10203},
  series = {Lecture Notes in Computer Science},
  isbn = {978-3-662-54458-7},
}

@mastersthesis{felicissimo:hal-03343699,
  title = {Representing Agda and coinduction in the $\lambda$$\Pi$-calculus modulo rewriting},
  author = {Felicissimo, Thiago},
  year = {2021},
  month = {Sep},
  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},
}

@inproceedings{Kahl14,
  title = {A Mechanised Abstract Formalisation of Concept Lattices},
  author = {Wolfram Kahl},
  year = {2014},
  doi = {10.1007/978-3-319-06251-8_15},
  url = {http://dx.doi.org/10.1007/978-3-319-06251-8_15},
  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 = {Peter Höfner and Peter Jipsen and Wolfram Kahl and Martin Eric Müller},
  volume = {8428},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-06250-1},
}

@inproceedings{CapperN12,
  title = {Towards a formal semantics for a structurally dynamic noncausal modelling language},
  author = {John Capper and Henrik Nilsson},
  year = {2012},
  doi = {10.1145/2103786.2103792},
  url = {http://doi.acm.org/10.1145/2103786.2103792},
  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 = {Benjamin C. Pierce},
  publisher = {ACM},
  isbn = {978-1-4503-1120-5},
}

@article{KaposiKA19,
  title = {Constructing quotient inductive-inductive types},
  author = {Ambrus Kaposi and András Kovács and Thorsten Altenkirch},
  year = {2019},
  url = {https://dl.acm.org/citation.cfm?id=3290315},
  researchr = {https://researchr.org/publication/KaposiKA19},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
}

@inproceedings{Kovacs22,
  title = {Generalized Universe Hierarchies and First-Class Universe Levels},
  author = {András Kovács},
  year = {2022},
  doi = {10.4230/LIPIcs.CSL.2022.28},
  url = {https://doi.org/10.4230/LIPIcs.CSL.2022.28},
  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 = {Florin Manea and Alex Simpson},
  volume = {216},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-218-1},
}

@inproceedings{JeffreyR11,
  title = {The Lax Braided Structure of Streaming I/O},
  author = {Alan Jeffrey and Julian Rathke},
  year = {2011},
  doi = {10.4230/LIPIcs.CSL.2011.292},
  url = {http://dx.doi.org/10.4230/LIPIcs.CSL.2011.292},
  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 = {Marc Bezem},
  volume = {12},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-939897-32-3},
}

@inproceedings{RouvoetPKV20,
  title = {Intrinsically-typed definitional interpreters for linear, session-typed languages},
  author = {Arjen Rouvoet and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser},
  year = {2020},
  doi = {10.1145/3372885.3373818},
  url = {https://doi.org/10.1145/3372885.3373818},
  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 = {Jasmin Blanchette and Catalin Hritcu},
  publisher = {ACM},
  isbn = {978-1-4503-7097-4},
}

@inproceedings{LicataZH08,
  title = {Focusing on Binding and Computation},
  author = {Daniel R. Licata and Noam Zeilberger and Robert Harper},
  year = {2008},
  doi = {10.1109/LICS.2008.48},
  url = {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},
}

@inproceedings{FavoniaFLL16,
  title = {A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory},
  author = {Kuen-Bang Hou (Favonia) and Eric Finster and Daniel R. Licata and Peter LeFanu Lumsdaine},
  year = {2016},
  doi = {10.1145/2933575.2934545},
  url = {http://doi.acm.org/10.1145/2933575.2934545},
  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 = {Martin Grohe and Eric Koskinen and Natarajan Shankar},
  publisher = {ACM},
  isbn = {978-1-4503-4391-6},
}

@inproceedings{BoveDS09,
  title = {Embedding a logical theory of constructions in Agda},
  author = {Ana Bove and Peter Dybjer and Andrés Sicard-Ramírez},
  year = {2009},
  doi = {10.1145/1481848.1481857},
  url = {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 = {Thorsten Altenkirch and Todd D. Millstein},
  publisher = {ACM},
  isbn = {978-1-60558-330-3},
}

@inproceedings{AltenkirchM09,
  title = {Indexed Containers},
  author = {Thorsten Altenkirch and Peter Morris},
  year = {2009},
  doi = {10.1109/LICS.2009.33},
  url = {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},
}

@inproceedings{FavoniaS16,
  title = {The Seifert-van Kampen Theorem in Homotopy Type Theory},
  author = {Kuen-Bang Hou (Favonia) and Michael Shulman},
  year = {2016},
  doi = {10.4230/LIPIcs.CSL.2016.22},
  url = {http://dx.doi.org/10.4230/LIPIcs.CSL.2016.22},
  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 = {Jean-Marc Talbot and Laurent Regnier},
  volume = {62},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-95977-022-4},
}

@inproceedings{GeestS17,
  title = {Generic packet descriptions: verified parsing and pretty printing of low-level data},
  author = {Marcell van Geest and Wouter Swierstra},
  year = {2017},
  doi = {10.1145/3122975.3122979},
  url = {https://doi.org/10.1145/3122975.3122979},
  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 = {Sam Lindley and Brent A. Yorgey},
  publisher = {ACM},
  isbn = {978-1-4503-5183-6},
}

@article{AltenkirchGHMM15,
  title = {Indexed containers},
  author = {Thorsten Altenkirch and Neil Ghani and Peter Hancock and Conor McBride and Peter Morris},
  year = {2015},
  doi = {10.1017/S095679681500009X},
  url = {http://dx.doi.org/10.1017/S095679681500009X},
  researchr = {https://researchr.org/publication/AltenkirchGHMM15},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {25},
}

@phdthesis{ethos-10314,
  title = {A continuous computational interpretation of type theories},
  author = {Chuangjie Xu},
  year = {2015},
  url = {http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.649340},
  note = {British Library, EThOS},
  researchr = {https://researchr.org/publication/ethos-10314},
  cites = {0},
  citedby = {0},
  school = {University of Birmingham, UK},
}

@inproceedings{PrinzKL22,
  title = {Deeper Shallow Embeddings},
  author = {Jacob Prinz and G. A. Kavvos and Leonidas Lampropoulos},
  year = {2022},
  doi = {10.4230/LIPIcs.ITP.2022.28},
  url = {https://doi.org/10.4230/LIPIcs.ITP.2022.28},
  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 = {June Andronick and Leonardo de Moura},
  volume = {237},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-252-5},
}

@article{UustaluVZ18,
  title = {The Sequent Calculus of Skew Monoidal Categories},
  author = {Tarmo Uustalu and Niccolò Veltri and Noam Zeilberger},
  year = {2018},
  doi = {10.1016/j.entcs.2018.11.017},
  url = {https://doi.org/10.1016/j.entcs.2018.11.017},
  researchr = {https://researchr.org/publication/UustaluVZ18},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {341},
  pages = {345-370},
}

@inproceedings{WeirichC10,
  title = {Arity-generic datatype-generic programming},
  author = {Stephanie Weirich and Chris Casinghino},
  year = {2010},
  doi = {10.1145/1707790.1707799},
  url = {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 = {Cormac Flanagan and Jean-Christophe Filliâtre},
  publisher = {ACM},
  isbn = {978-1-60558-890-2},
}

@article{CockxD18,
  title = {Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory},
  author = {Jesper Cockx and Dominique Devriese},
  year = {2018},
  doi = {10.1017/S095679681800014X},
  url = {https://doi.org/10.1017/S095679681800014X},
  researchr = {https://researchr.org/publication/CockxD18},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {28},
}

@inproceedings{Norell08,
  title = {Dependently Typed Programming in Agda},
  author = {Ulf Norell},
  year = {2008},
  doi = {10.1007/978-3-642-04652-0_5},
  url = {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 = {Pieter W. M. Koopman and Rinus Plasmeijer and S. Doaitse Swierstra},
  volume = {5832},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-04651-3},
}

@inproceedings{ChapmanDMM10,
  title = {The gentle art of levitation},
  author = {James Chapman and Pierre-Évariste Dagand and Conor McBride and Peter Morris},
  year = {2010},
  doi = {10.1145/1863543.1863547},
  url = {http://doi.acm.org/10.1145/1863543.1863547},
  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 = {Paul Hudak and Stephanie Weirich},
  publisher = {ACM},
  isbn = {978-1-60558-794-3},
}

@article{RestS22,
  title = {A completely unique account of enumeration},
  author = {Cas van der Rest and Wouter Swierstra},
  year = {2022},
  doi = {10.1145/3547636},
  url = {https://doi.org/10.1145/3547636},
  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},
}

@inproceedings{CicconeP20,
  title = {A Dependently Typed Linear π-Calculus in Agda},
  author = {Luca Ciccone and Luca Padovani},
  year = {2020},
  doi = {10.1145/3414080.3414109},
  url = {https://doi.org/10.1145/3414080.3414109},
  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},
}

@inproceedings{OrtonP16,
  title = {Axioms for Modelling Cubical Type Theory in a Topos},
  author = {Ian Orton and Andrew M. Pitts},
  year = {2016},
  doi = {10.4230/LIPIcs.CSL.2016.24},
  url = {http://dx.doi.org/10.4230/LIPIcs.CSL.2016.24},
  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 = {Jean-Marc Talbot and Laurent Regnier},
  volume = {62},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-95977-022-4},
}

@inproceedings{BoveD08,
  title = {Dependent Types at Work},
  author = {Ana Bove and Peter Dybjer},
  year = {2008},
  doi = {10.1007/978-3-642-03153-3_2},
  url = {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 = {Ana Bove and Luís Soares Barbosa and Alberto Pardo and Jorge Sousa Pinto},
  volume = {5520},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-03152-6},
}

@article{StuckiG21,
  title = {A theory of higher-order subtyping with type intervals},
  author = {Sandro Stucki and  Paolo G. Giarrusso},
  year = {2021},
  doi = {10.1145/3473574},
  url = {https://doi.org/10.1145/3473574},
  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},
}

@inproceedings{MiraldoCMSS21,
  title = {Formal verification of authenticated, append-only skip lists in Agda},
  author = {Victor Cacciari Miraldo and Harold Carr and Mark Moir and Lisandra Silva and Guy L. Steele Jr.},
  year = {2021},
  doi = {10.1145/3437992.3439924},
  url = {https://doi.org/10.1145/3437992.3439924},
  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 = {Catalin Hritcu and Andrei Popescu 0001},
  publisher = {ACM},
  isbn = {978-1-4503-8299-1},
}

@inproceedings{HuH09-9,
  title = {Compiling Concurrency Correctly: Cutting out the Middle Man},
  author = {Liyang Hu and Graham Hutton},
  year = {2009},
  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 = {Zoltán Horváth and Viktória Zsók and Peter Achten and Pieter W. M. Koopman},
  volume = {10},
  series = {Trends in Functional Programming},
  publisher = {Intellect},
  isbn = {978-1-84150-405-6},
}

@inproceedings{KokkeS15,
  title = {Auto in Agda - Programming Proof Search Using Reflection},
  author = {Pepijn Kokke and Wouter Swierstra},
  year = {2015},
  doi = {10.1007/978-3-319-19797-5_14},
  url = {http://dx.doi.org/10.1007/978-3-319-19797-5_14},
  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 = {Ralf Hinze and Janis Voigtländer},
  volume = {9129},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-19796-8},
}

@inproceedings{AbelV14,
  title = {A Formalized Proof of Strong Normalization for Guarded Recursive Types},
  author = {Andreas Abel and Andrea Vezzosi},
  year = {2014},
  doi = {10.1007/978-3-319-12736-1_8},
  url = {http://dx.doi.org/10.1007/978-3-319-12736-1_8},
  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 = {Jacques Garrigue},
  volume = {8858},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-12735-4},
}

@inproceedings{Danielsson10-1,
  title = {Beating the Productivity Checker Using Embedded Languages},
  author = {Nils Anders Danielsson},
  year = {2010},
  url = {http://www.easychair.org/publications/?page=350518201},
  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 = {Ekaterina Komendantskaya and Ana Bove and Milad Niqui},
  volume = {5},
  series = {EPiC Series},
  publisher = {EasyChair},
}

@article{AngiuliMLH16,
  title = {Homotopical patch theory},
  author = {Carlo Angiuli and Edward Morehouse and Daniel R. Licata and Robert Harper},
  year = {2016},
  doi = {10.1017/S0956796816000198},
  url = {http://dx.doi.org/10.1017/S0956796816000198},
  researchr = {https://researchr.org/publication/AngiuliMLH16},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {26},
}

@inproceedings{Jeffrey13-1,
  title = {Dependently Typed Web Client Applications - FRP in Agda in HTML5},
  author = {Alan Jeffrey},
  year = {2013},
  doi = {10.1007/978-3-642-45284-0_16},
  url = {http://dx.doi.org/10.1007/978-3-642-45284-0_16},
  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 = {Konstantinos F. Sagonas},
  volume = {7752},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-45283-3},
}

@inproceedings{HuC21,
  title = {Formalizing category theory in Agda},
  author = {Jason Z. S. Hu and Jacques Carette},
  year = {2021},
  doi = {10.1145/3437992.3439922},
  url = {https://doi.org/10.1145/3437992.3439922},
  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 = {Catalin Hritcu and Andrei Popescu 0001},
  publisher = {ACM},
  isbn = {978-1-4503-8299-1},
}

@inproceedings{LicataH09-0,
  title = {Positively dependent types},
  author = {Daniel R. Licata and Robert Harper},
  year = {2009},
  doi = {10.1145/1481848.1481851},
  url = {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 = {Thorsten Altenkirch and Todd D. Millstein},
  publisher = {ACM},
  isbn = {978-1-60558-330-3},
}

@inproceedings{IonescuJ12,
  title = {Dependently-Typed Programming in Scientific Computing - Examples from Economic Modelling},
  author = {Cezar Ionescu and Patrik Jansson},
  year = {2012},
  doi = {10.1007/978-3-642-41582-1_9},
  url = {http://dx.doi.org/10.1007/978-3-642-41582-1_9},
  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 = {Ralf Hinze},
  volume = {8241},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-41581-4},
}

@inproceedings{DevrieseP11-1,
  title = {On the bright side of type classes: instance arguments in Agda},
  author = {Dominique Devriese and Frank Piessens},
  year = {2011},
  doi = {10.1145/2034773.2034796},
  url = {http://doi.acm.org/10.1145/2034773.2034796},
  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 = {Manuel M. T. Chakravarty and Zhenjiang Hu and Olivier Danvy},
  publisher = {ACM},
  isbn = {978-1-4503-0865-6},
}

@article{Chapman09,
  title = {Type Theory Should Eat Itself},
  author = {James Chapman},
  year = {2009},
  doi = {10.1016/j.entcs.2008.12.114},
  url = {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},
}

@inproceedings{Zeilberger08,
  title = {Focusing and higher-order abstract syntax},
  author = {Noam Zeilberger},
  year = {2008},
  doi = {10.1145/1328438.1328482},
  url = {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 = {George C. Necula and Philip Wadler},
  publisher = {ACM},
  isbn = {978-1-59593-689-9},
}

@article{BernardyJP12,
  title = {Proofs for free - Parametricity for dependent types},
  author = {Jean-Philippe Bernardy and Patrik Jansson and Ross Paterson},
  year = {2012},
  doi = {10.1017/S0956796812000056},
  url = {http://dx.doi.org/10.1017/S0956796812000056},
  researchr = {https://researchr.org/publication/BernardyJP12},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {22},
  number = {2},
  pages = {107-152},
}

@inproceedings{GhaniMFS13,
  title = {Fibred Data Types},
  author = {Neil Ghani and Lorenzo Malatesta and Fredrik Nordvall Forsberg and Anton Setzer},
  year = {2013},
  doi = {10.1109/LICS.2013.30},
  url = {http://doi.ieeecomputersociety.org/10.1109/LICS.2013.30},
  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},
}

@inproceedings{BoveDN09,
  title = {A Brief Overview of Agda - A Functional Language with Dependent Types},
  author = {Ana Bove and Peter Dybjer and Ulf Norell},
  year = {2009},
  doi = {10.1007/978-3-642-03359-9_6},
  url = {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 = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
  volume = {5674},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-03358-2},
}

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

@article{EscardoS16,
  title = {The intrinsic topology of Martin-Löf universes},
  author = {Martín Hötzel Escardó and Thomas Streicher},
  year = {2016},
  doi = {10.1016/j.apal.2016.04.010},
  url = {http://dx.doi.org/10.1016/j.apal.2016.04.010},
  researchr = {https://researchr.org/publication/EscardoS16},
  cites = {0},
  citedby = {0},
  journal = {Annals of Pure and Applied Logic},
  volume = {167},
  number = {9},
  pages = {794-805},
}

@inproceedings{AltenkirchK16,
  title = {Type theory in type theory using quotient inductive types},
  author = {Thorsten Altenkirch and Ambrus Kaposi},
  year = {2016},
  doi = {10.1145/2837614.2837638},
  url = {http://doi.acm.org/10.1145/2837614.2837638},
  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 = {Rastislav Bodik and Rupak Majumdar},
  publisher = {ACM},
  isbn = {978-1-4503-3549-2},
}

@misc{https:-doi.org-10.48550-arxiv.2103.05581,
  title = {The Agda Universal Algebra Library, Part 1: Foundation},
  author = {DeMeo, William},
  year = {2021},
  doi = {10.48550/ARXIV.2103.05581},
  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},
}

@inproceedings{AltenkirchCU10,
  title = {Monads Need Not Be Endofunctors},
  author = {Thorsten Altenkirch and James Chapman and Tarmo Uustalu},
  year = {2010},
  doi = {10.1007/978-3-642-12032-9_21},
  url = {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 = {C.-H. Luke Ong},
  volume = {6014},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-12031-2},
}

@inproceedings{SerranoM18,
  title = {Generic programming of all kinds},
  author = {Alejandro Serrano and Victor Cacciari Miraldo},
  year = {2018},
  doi = {10.1145/3242744.3242745},
  url = {https://doi.org/10.1145/3242744.3242745},
  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 = {Nicolas Wu},
  publisher = {ACM},
}

@inproceedings{AtkeyJG11,
  title = {When Is a Type Refinement an Inductive Type?},
  author = {Robert Atkey and Patricia Johann and Neil Ghani},
  year = {2011},
  doi = {10.1007/978-3-642-19805-2_6},
  url = {http://dx.doi.org/10.1007/978-3-642-19805-2_6},
  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 = {Martin Hofmann},
  volume = {6604},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-19804-5},
}

@inproceedings{Allais0MM17,
  title = {Type-and-scope safe programs and their proofs},
  author = {Guillaume Allais and James Chapman and Conor McBride and James McKinna},
  year = {2017},
  doi = {10.1145/3018610.3018613},
  url = {http://doi.acm.org/10.1145/3018610.3018613},
  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 = {Yves Bertot and Viktor Vafeiadis},
  publisher = {ACM},
  isbn = {978-1-4503-4705-1},
}

@inproceedings{PouillardP10,
  title = {A fresh look at programming with names and binders},
  author = {Nicolas Pouillard and François Pottier},
  year = {2010},
  doi = {10.1145/1863543.1863575},
  url = {http://doi.acm.org/10.1145/1863543.1863575},
  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 = {Paul Hudak and Stephanie Weirich},
  publisher = {ACM},
  isbn = {978-1-60558-794-3},
}

@inproceedings{Benjamin21-0,
  title = {Formalisation of Dependent Type Theory: The Example of CaTT},
  author = {Thibaut Benjamin},
  year = {2021},
  doi = {10.4230/LIPIcs.TYPES.2021.2},
  url = {https://doi.org/10.4230/LIPIcs.TYPES.2021.2},
  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 = {Henning Basold and Jesper Cockx and Silvia Ghilezan},
  volume = {239},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-254-9},
}

@article{MuKJ09,
  title = {Algebra of programming in Agda: Dependent types for relational program derivation},
  author = {Shin-Cheng Mu and Hsiang-Shang Ko and Patrik Jansson},
  year = {2009},
  doi = {10.1017/S0956796809007345},
  url = {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},
}

@article{Dagand17,
  title = {The essence of ornaments},
  author = {Pierre-Évariste Dagand},
  year = {2017},
  doi = {10.1017/S0956796816000356},
  url = {http://dx.doi.org/10.1017/S0956796816000356},
  researchr = {https://researchr.org/publication/Dagand17},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {27},
}

@misc{https:-doi.org-10.48550-arxiv.2104.04095,
  title = {First-order natural deduction in Agda},
  author = {Warren, Louis},
  year = {2021},
  doi = {10.48550/ARXIV.2104.04095},
  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},
}

@misc{https:-doi.org-10.48550-arxiv.2205.08718,
  title = {An approach to translating Haskell programs to Agda and reasoning about them},
  author = {Carr, Harold and Jenkins, Christa and Moir, Mark and Miraldo, Victor Cacciari and Silva, Lisandra},
  year = {2022},
  doi = {10.48550/ARXIV.2205.08718},
  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},
}

@inproceedings{LicataS13,
  title = {Calculating the Fundamental Group of the Circle in Homotopy Type Theory},
  author = {Daniel R. Licata and Michael Shulman},
  year = {2013},
  doi = {10.1109/LICS.2013.28},
  url = {http://doi.ieeecomputersociety.org/10.1109/LICS.2013.28},
  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},
}

@inproceedings{Danielsson12-0,
  title = {Operational semantics using the partiality monad},
  author = {Nils Anders Danielsson},
  year = {2012},
  doi = {10.1145/2364527.2364546},
  url = {http://doi.acm.org/10.1145/2364527.2364546},
  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 = {Peter Thiemann and Robby Bruce Findler},
  publisher = {ACM},
  isbn = {978-1-4503-1054-3},
}

@inproceedings{SculthorpeN09,
  title = {Safe functional reactive programming through dependent types},
  author = {Neil Sculthorpe and Henrik Nilsson},
  year = {2009},
  doi = {10.1145/1596550.1596558},
  url = {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 = {Graham Hutton and Andrew P. Tolmach},
  publisher = {ACM},
  isbn = {978-1-60558-332-7},
}

@article{GuntherGP18,
  title = {Formalization of Universal Algebra in Agda},
  author = {Emmanuel Gunther and Alejandro Gadea and Miguel Pagano},
  year = {2018},
  doi = {10.1016/j.entcs.2018.10.010},
  url = {https://doi.org/10.1016/j.entcs.2018.10.010},
  researchr = {https://researchr.org/publication/GuntherGP18},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {338},
  pages = {147-166},
}

@article{PujetT23,
  title = {Impredicative Observational Equality},
  author = {Loïc Pujet and Nicolas Tabareau},
  year = {2023},
  month = {January},
  doi = {10.1145/3571739},
  url = {https://doi.org/10.1145/3571739},
  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},
}

@inproceedings{DanielssonN08,
  title = {Parsing Mixfix Operators},
  author = {Nils Anders Danielsson and Ulf Norell},
  year = {2008},
  doi = {10.1007/978-3-642-24452-0_5},
  url = {http://dx.doi.org/10.1007/978-3-642-24452-0_5},
  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 = {Sven-Bodo Scholz and Olaf Chitil},
  volume = {5836},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-24451-3},
}

@inproceedings{CockxDP16,
  title = {Unifiers as equivalences: proof-relevant unification of dependently typed data},
  author = {Jesper Cockx and Dominique Devriese and Frank Piessens},
  year = {2016},
  doi = {10.1145/2951913.2951917},
  url = {http://doi.acm.org/10.1145/2951913.2951917},
  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 = {Jacques Garrigue and Gabriele Keller and Eijiro Sumii},
  publisher = {ACM},
  isbn = {978-1-4503-4219-3},
}

@inproceedings{CockxDP14,
  title = {Pattern matching without K},
  author = {Jesper Cockx and Dominique Devriese and Frank Piessens},
  year = {2014},
  doi = {10.1145/2628136.2628139},
  url = {http://doi.acm.org/10.1145/2628136.2628139},
  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 = {Johan Jeuring and Manuel M. T. Chakravarty},
  publisher = {ACM},
  isbn = {978-1-4503-2873-9},
}

@article{CockxA18,
  title = {Elaborating dependent (co)pattern matching},
  author = {Jesper Cockx and Andreas Abel},
  year = {2018},
  doi = {10.1145/3236770},
  url = {https://doi.org/10.1145/3236770},
  researchr = {https://researchr.org/publication/CockxA18},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {ICFP},
}

@inproceedings{Kraus16,
  title = {Constructions with Non-Recursive Higher Inductive Types},
  author = {Nicolai Kraus},
  year = {2016},
  doi = {10.1145/2933575.2933586},
  url = {http://doi.acm.org/10.1145/2933575.2933586},
  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 = {Martin Grohe and Eric Koskinen and Natarajan Shankar},
  publisher = {ACM},
  isbn = {978-1-4503-4391-6},
}

@inproceedings{Jeffrey12,
  title = {LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs},
  author = {Alan Jeffrey},
  year = {2012},
  doi = {10.1145/2103776.2103783},
  url = {http://doi.acm.org/10.1145/2103776.2103783},
  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 = {Koen Claessen and Nikhil Swamy},
  publisher = {ACM},
  isbn = {978-1-4503-1125-0},
}

@inproceedings{Danielsson10,
  title = {Total parser combinators},
  author = {Nils Anders Danielsson},
  year = {2010},
  doi = {10.1145/1863543.1863585},
  url = {http://doi.acm.org/10.1145/1863543.1863585},
  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 = {Paul Hudak and Stephanie Weirich},
  publisher = {ACM},
  isbn = {978-1-60558-794-3},
}

@article{KidneyW21,
  title = {Algebras for weighted search},
  author = {Donnacha Oisín Kidney and Nicolas Wu},
  year = {2021},
  doi = {10.1145/3473577},
  url = {https://doi.org/10.1145/3473577},
  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},
}

@inproceedings{CapperN10,
  title = {Static Balance Checking for First-Class Modular Systems of Equations},
  author = {John Capper and Henrik Nilsson},
  year = {2010},
  doi = {10.1007/978-3-642-22941-1_4},
  url = {http://dx.doi.org/10.1007/978-3-642-22941-1_4},
  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 = {Rex L. Page and Zoltán Horváth and Viktória Zsók},
  volume = {6546},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-22940-4},
}

@article{AhrensHLM20,
  title = {Reduction monads and their signatures},
  author = {Benedikt Ahrens and André Hirschowitz and Ambroise Lafont and Marco Maggesi},
  year = {2020},
  doi = {10.1145/3371099},
  url = {https://doi.org/10.1145/3371099},
  researchr = {https://researchr.org/publication/AhrensHLM20},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {POPL},
}

@article{AhmanS13,
  title = {Normalization by Evaluation and Algebraic Effects},
  author = {Danel Ahman and Sam Staton},
  year = {2013},
  doi = {10.1016/j.entcs.2013.09.007},
  url = {http://dx.doi.org/10.1016/j.entcs.2013.09.007},
  researchr = {https://researchr.org/publication/AhmanS13},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {298},
  pages = {51-69},
}

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

@inproceedings{Coquand06,
  title = {Alfa/Agda},
  author = {Thierry Coquand},
  year = {2006},
  doi = {10.1007/11542384_9},
  url = {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 = {Freek Wiedijk},
  volume = {3600},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-30704-4},
}

@inproceedings{WaltS12,
  title = {Engineering Proof by Reflection in Agda},
  author = {Paul van der Walt and Wouter Swierstra},
  year = {2012},
  doi = {10.1007/978-3-642-41582-1_10},
  url = {http://dx.doi.org/10.1007/978-3-642-41582-1_10},
  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 = {Ralf Hinze},
  volume = {8241},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-41581-4},
}

@inproceedings{UrciuoliTS20,
  title = {Strong Normalization for the Simply-Typed Lambda Calculus in Constructive Type Theory Using Agda},
  author = {Sebastián Urciuoli and Álvaro Tasistro and Nora Szasz},
  year = {2020},
  doi = {10.1016/j.entcs.2020.08.010},
  url = {https://doi.org/10.1016/j.entcs.2020.08.010},
  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 = {Cláudia Nalon},
  volume = {351},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier},
}

@article{0001P16-8,
  title = {Well-founded recursion with copatterns and sized types},
  author = {Andreas Abel and Brigitte Pientka},
  year = {2016},
  doi = {10.1017/S0956796816000022},
  url = {http://dx.doi.org/10.1017/S0956796816000022},
  researchr = {https://researchr.org/publication/0001P16-8},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {26},
}

@misc{https:-doi.org-10.48550-arxiv.2110.05771,
  title = {Toward SMT-Based Refinement Types in Agda},
  author = {Shen, Gan and Kuper, Lindsey},
  year = {2021},
  doi = {10.48550/ARXIV.2110.05771},
  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},
}

@inproceedings{Zeilberger09,
  title = {Refinement types and computational duality},
  author = {Noam Zeilberger},
  year = {2009},
  doi = {10.1145/1481848.1481852},
  url = {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 = {Thorsten Altenkirch and Todd D. Millstein},
  publisher = {ACM},
  isbn = {978-1-60558-330-3},
}

@inproceedings{FelicissimoBB23,
  title = {Translating Proofs from an Impredicative Type System to a Predicative One},
  author = {Thiago Felicissimo and Frédéric Blanqui and Ashish Kumar Barnawal},
  year = {2023},
  doi = {10.4230/LIPIcs.CSL.2023.19},
  url = {https://doi.org/10.4230/LIPIcs.CSL.2023.19},
  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 = {Bartek Klin and Elaine Pimentel},
  volume = {252},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-264-8},
}

@inproceedings{Allais19,
  title = {Generic level polymorphic n-ary functions},
  author = {Guillaume Allais},
  year = {2019},
  doi = {10.1145/3331554.3342604},
  url = {https://doi.org/10.1145/3331554.3342604},
  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 = {David Darais and Jeremy Gibbons},
  publisher = {ACM},
  isbn = {978-1-4503-6815-5},
}

@article{ChapmanUV19,
  title = {Quotienting the delay monad by weak bisimilarity},
  author = {James Chapman and Tarmo Uustalu and Niccolò Veltri},
  year = {2019},
  doi = {10.1017/S0960129517000184},
  url = {https://doi.org/10.1017/S0960129517000184},
  researchr = {https://researchr.org/publication/ChapmanUV19},
  cites = {0},
  citedby = {0},
  journal = {Mathematical Structures in Computer Science},
  volume = {29},
  number = {1},
  pages = {67-92},
}

@inproceedings{IonescuJ11,
  title = {Testing versus proving in climate impact research},
  author = {Cezar Ionescu and Patrik Jansson},
  year = {2011},
  doi = {10.4230/LIPIcs.TYPES.2011.41},
  url = {http://dx.doi.org/10.4230/LIPIcs.TYPES.2011.41},
  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 = {Nils Anders Danielsson and Bengt Nordström},
  volume = {19},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-939897-49-1},
}

@inproceedings{HamanaF11,
  title = {A foundation for GADTs and inductive families: dependent polynomial functor approach},
  author = {Makoto Hamana and Marcelo P. Fiore},
  year = {2011},
  doi = {10.1145/2036918.2036927},
  url = {http://doi.acm.org/10.1145/2036918.2036927},
  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 = {Jaakko Järvi and Shin-Cheng Mu},
  publisher = {ACM},
  isbn = {978-1-4503-0861-8},
}

@inproceedings{LicataS16,
  title = {Adjoint Logic with a 2-Category of Modes},
  author = {Daniel R. Licata and Michael Shulman},
  year = {2016},
  doi = {10.1007/978-3-319-27683-0_16},
  url = {http://dx.doi.org/10.1007/978-3-319-27683-0_16},
  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 = {Sergei N. Artëmov and Anil Nerode},
  volume = {9537},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-27682-3},
}

@inproceedings{Danielsson08,
  title = {Lightweight semiformal time complexity analysis for purely functional data structures},
  author = {Nils Anders Danielsson},
  year = {2008},
  doi = {10.1145/1328438.1328457},
  url = {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 = {George C. Necula and Philip Wadler},
  publisher = {ACM},
  isbn = {978-1-59593-689-9},
}

@article{Bove09,
  title = {Another Look at Function Domains},
  author = {Ana Bove},
  year = {2009},
  doi = {10.1016/j.entcs.2009.07.084},
  url = {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},
}

@inproceedings{Takeyama11,
  title = {Programming assurance cases in Agda},
  author = {Makoto Takeyama},
  year = {2011},
  doi = {10.1145/2034773.2034794},
  url = {http://doi.acm.org/10.1145/2034773.2034794},
  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 = {Manuel M. T. Chakravarty and Zhenjiang Hu and Olivier Danvy},
  publisher = {ACM},
  isbn = {978-1-4503-0865-6},
}

@inproceedings{AsaiFTZ14,
  title = {A Type Theoretic Specification of Partial Evaluation},
  author = {Kenichi Asai and Luminous Fennell and Peter Thiemann and Yang Zhang},
  year = {2014},
  doi = {10.1145/2643135.2643146},
  url = {http://doi.acm.org/10.1145/2643135.2643146},
  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 = {Olaf Chitil and Andy King and Olivier Danvy},
  publisher = {ACM},
  isbn = {978-1-4503-2947-7},
}

@inproceedings{FirsovU15-0,
  title = {Dependently typed programming with finite sets},
  author = {Denis Firsov and Tarmo Uustalu},
  year = {2015},
  doi = {10.1145/2808098.2808102},
  url = {http://doi.acm.org/10.1145/2808098.2808102},
  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 = {Patrick Bahr and Sebastian Erdweg},
  publisher = {ACM},
  isbn = {978-1-4503-3810-3},
}

@article{SwierstraB19,
  title = {A predicate transformer semantics for effects (functional pearl)},
  author = {Wouter Swierstra and Tim Baanen},
  year = {2019},
  doi = {10.1145/3341707},
  url = {https://doi.org/10.1145/3341707},
  researchr = {https://researchr.org/publication/SwierstraB19},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
}

@inproceedings{ForsbergXG20,
  title = {Three equivalent ordinal notation systems in cubical Agda},
  author = {Fredrik Nordvall Forsberg and Chuangjie Xu and Neil Ghani},
  year = {2020},
  doi = {10.1145/3372885.3373835},
  url = {https://doi.org/10.1145/3372885.3373835},
  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 = {Jasmin Blanchette and Catalin Hritcu},
  publisher = {ACM},
  isbn = {978-1-4503-7097-4},
}

@inproceedings{from2021teaching,
  title = {Teaching automated reasoning and formally verified functional programming in Agda and Isabelle/HOL},
  author = {From, Asta Halkjær  and Villadsen, Jørgen },
  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},
}

@article{KokkeSW20,
  title = {Programming language foundations in Agda},
  author = {Wen Kokke and Jeremy G. Siek and Philip Wadler},
  year = {2020},
  doi = {10.1016/j.scico.2020.102440},
  url = {https://doi.org/10.1016/j.scico.2020.102440},
  researchr = {https://researchr.org/publication/KokkeSW20},
  cites = {0},
  citedby = {0},
  journal = {Science of Computer Programming},
  volume = {194},
  pages = {102440},
}

@inproceedings{OmarVHAH17,
  title = {Hazelnut: a bidirectionally typed structure editor calculus},
  author = {Cyrus Omar and Ian Voysey and Michael Hilton and Jonathan Aldrich and Matthew A. Hammer},
  year = {2017},
  url = {http://dl.acm.org/citation.cfm?id=3009900},
  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 = {Giuseppe Castagna and Andrew D. Gordon},
  publisher = {ACM},
  isbn = {978-1-4503-4660-3},
}

@inproceedings{McBride15,
  title = {Turing-Completeness Totally Free},
  author = {Conor McBride},
  year = {2015},
  doi = {10.1007/978-3-319-19797-5_13},
  url = {http://dx.doi.org/10.1007/978-3-319-19797-5_13},
  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 = {Ralf Hinze and Janis Voigtländer},
  volume = {9129},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-19796-8},
}

@inproceedings{SpallMT22,
  title = {Forward build systems, formally},
  author = {Sarah Spall and Neil Mitchell and Sam Tobin-Hochstadt},
  year = {2022},
  doi = {10.1145/3497775.3503687},
  url = {https://doi.org/10.1145/3497775.3503687},
  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 = {Andrei Popescu 0001 and Steve Zdancewic},
  publisher = {ACM},
  isbn = {978-1-4503-9182-5},
}

@inproceedings{EscardoX15,
  title = {The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard Interpretation},
  author = {Martín Hötzel Escardó and Chuangjie Xu},
  year = {2015},
  doi = {10.4230/LIPIcs.TLCA.2015.153},
  url = {http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.153},
  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 = {Thorsten Altenkirch},
  volume = {38},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-939897-87-3},
}

@inproceedings{ChengHM18,
  title = {Functional Pearl: Folding Polynomials of Polynomials},
  author = {Chen-Mou Cheng and Ruey-Lin Hsu and Shin-Cheng Mu},
  year = {2018},
  doi = {10.1007/978-3-319-90686-7_5},
  url = {https://doi.org/10.1007/978-3-319-90686-7_5},
  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 = {John P. Gallagher and Martin Sulzmann},
  volume = {10818},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-90686-7},
}

@inproceedings{SwierstraA08,
  title = {Dependent Types for Distributed Arrays},
  author = {Wouter Swierstra and Thorsten Altenkirch},
  year = {2008},
  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 = {Peter Achten and Pieter W. M. Koopman and Marco T. Morazán},
  volume = {9},
  series = {Trends in Functional Programming},
  publisher = {Intellect},
  isbn = {978-1-84150-277-9},
}

@inproceedings{AhmanCU12,
  title = {When Is a Container a Comonad?},
  author = {Danel Ahman and James Chapman and Tarmo Uustalu},
  year = {2012},
  doi = {10.1007/978-3-642-28729-9_5},
  url = {http://dx.doi.org/10.1007/978-3-642-28729-9_5},
  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 = {Lars Birkedal},
  volume = {7213},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-28728-2},
}

@article{LabradaTTD22,
  title = {Plausible sealing for gradual parametricity},
  author = {Elizabeth Labrada and Matías Toro and Éric Tanter and Dominique Devriese},
  year = {2022},
  doi = {10.1145/3527314},
  url = {https://doi.org/10.1145/3527314},
  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},
}

@inproceedings{EscardoO10-1,
  title = {What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift Have in Common},
  author = {Martín Escardó and Paulo Oliva},
  year = {2010},
  doi = {10.1145/1863597.1863605},
  url = {http://doi.acm.org/10.1145/1863597.1863605},
  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 = {Venanzio Capretta and James Chapman 0001},
  publisher = {ACM},
  isbn = {978-1-4503-0255-5},
}

@inproceedings{MortbergP20,
  title = {Cubical synthetic homotopy theory},
  author = {Anders Mörtberg and Loïc Pujet},
  year = {2020},
  doi = {10.1145/3372885.3373825},
  url = {https://doi.org/10.1145/3372885.3373825},
  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 = {Jasmin Blanchette and Catalin Hritcu},
  publisher = {ACM},
  isbn = {978-1-4503-7097-4},
}

@inproceedings{JacobsND19,
  title = {How to do proofs: practically proving properties about effectful programs' results (functional pearl)},
  author = {Koen Jacobs and Andreas Nuyts and Dominique Devriese},
  year = {2019},
  doi = {10.1145/3331554.3342603},
  url = {https://doi.org/10.1145/3331554.3342603},
  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 = {David Darais and Jeremy Gibbons},
  publisher = {ACM},
  isbn = {978-1-4503-6815-5},
}

@inproceedings{OConnor19,
  title = {Deferring the details and deriving programs},
  author = {Liam O'Connor},
  year = {2019},
  doi = {10.1145/3331554.3342605},
  url = {https://doi.org/10.1145/3331554.3342605},
  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 = {David Darais and Jeremy Gibbons},
  publisher = {ACM},
  isbn = {978-1-4503-6815-5},
}

@article{AbelAS17,
  title = {Interactive programming in Agda - Objects and graphical user interfaces},
  author = {Andreas Abel and Stephan Adelsberger and Anton Setzer},
  year = {2017},
  doi = {10.1017/S0956796816000319},
  url = {http://dx.doi.org/10.1017/S0956796816000319},
  researchr = {https://researchr.org/publication/AbelAS17},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {27},
}

@inproceedings{EadesP16,
  title = {Multiple Conclusion Linear Logic: Cut Elimination and More},
  author = {Harley Eades III and Valeria de Paiva},
  year = {2016},
  doi = {10.1007/978-3-319-27683-0_7},
  url = {http://dx.doi.org/10.1007/978-3-319-27683-0_7},
  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 = {Sergei N. Artëmov and Anil Nerode},
  volume = {9537},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-27682-3},
}

@inproceedings{ZmigrodDG18,
  title = {An Agda Formalization of Üresin and Dubois' Asynchronous Fixed-Point Theory},
  author = {Ran Zmigrod and Matthew L. Daggitt and Timothy G. Griffin},
  year = {2018},
  doi = {10.1007/978-3-319-94821-8_37},
  url = {https://doi.org/10.1007/978-3-319-94821-8_37},
  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 = {Jeremy Avigad and Assia Mahboubi},
  volume = {10895},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-94821-8},
}

@article{ChenS21-1,
  title = {A computational interpretation of compact closed categories: reversible programming with negative and fractional types},
  author = {Chao-Hong Chen and Amr Sabry},
  year = {2021},
  doi = {10.1145/3434290},
  url = {https://doi.org/10.1145/3434290},
  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},
}

@inproceedings{NoortSAP11,
  title = {Embedding polymorphic dynamic typing},
  author = {Thomas van Noort and Wouter Swierstra and Peter Achten and Rinus Plasmeijer},
  year = {2011},
  doi = {10.1145/2036918.2036923},
  url = {http://doi.acm.org/10.1145/2036918.2036923},
  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 = {Jaakko Järvi and Shin-Cheng Mu},
  publisher = {ACM},
  isbn = {978-1-4503-0861-8},
}

@article{AhmanP21,
  title = {Asynchronous effects},
  author = {Danel Ahman and Matija Pretnar},
  year = {2021},
  doi = {10.1145/3434305},
  url = {https://doi.org/10.1145/3434305},
  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},
}

@inproceedings{Al-hassyK15,
  title = {Mechanised Relation-Algebraic Order Theory in Ordered Categories without Meets},
  author = {Musa Al-hassy and Wolfram Kahl},
  year = {2015},
  doi = {10.1007/978-3-319-24704-5_10},
  url = {http://dx.doi.org/10.1007/978-3-319-24704-5_10},
  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 = {Wolfram Kahl and Michael Winter and José N. Oliveira},
  volume = {9348},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-24703-8},
}

@article{EscardoX16,
  title = {A constructive manifestation of the Kleene-Kreisel continuous functionals},
  author = {Martín Escardó and Chuangjie Xu},
  year = {2016},
  doi = {10.1016/j.apal.2016.04.011},
  url = {http://dx.doi.org/10.1016/j.apal.2016.04.011},
  researchr = {https://researchr.org/publication/EscardoX16},
  cites = {0},
  citedby = {0},
  journal = {Annals of Pure and Applied Logic},
  volume = {167},
  number = {9},
  pages = {770-793},
}

@inproceedings{KoG11,
  title = {Modularising inductive families},
  author = {Hsiang-Shang Ko and Jeremy Gibbons},
  year = {2011},
  doi = {10.1145/2036918.2036921},
  url = {http://doi.acm.org/10.1145/2036918.2036921},
  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 = {Jaakko Järvi and Shin-Cheng Mu},
  publisher = {ACM},
  isbn = {978-1-4503-0861-8},
}

@article{Montin2022,
  title = {{LibNDT}: Towards a Formal Library on Spreadable Properties over Linked Nested Datatypes},
  author = {Mathieu Montin and Amélie Ledein and Catherine Dubois},
  year = {2022},
  month = {jun},
  doi = {10.4204/eptcs.360.2},
  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},
}

@inproceedings{CaretteF17,
  title = {Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study},
  author = {Jacques Carette and William M. Farmer},
  year = {2017},
  doi = {10.1007/978-3-319-62075-6_2},
  url = {https://doi.org/10.1007/978-3-319-62075-6_2},
  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 = {Herman Geuvers and Matthew England and Osman Hasan and Florian Rabe and Olaf Teschke},
  volume = {10383},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-62075-6},
}

@inproceedings{LindbladB04,
  title = {A Tool for Automated Theorem Proving in Agda},
  author = {Fredrik Lindblad and Marcin Benke},
  year = {2004},
  doi = {10.1007/11617990_10},
  url = {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 = {Jean-Christophe Filliâtre and Christine Paulin-Mohring and Benjamin Werner},
  volume = {3839},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-31428-8},
}

@article{SwierstraN13,
  title = {A library for polymorphic dynamic typing},
  author = {Wouter Swierstra and Thomas van Noort},
  year = {2013},
  doi = {10.1017/S0956796813000063},
  url = {http://dx.doi.org/10.1017/S0956796813000063},
  researchr = {https://researchr.org/publication/SwierstraN13},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {23},
  number = {3},
  pages = {229-248},
}

@inproceedings{BernardyJP10,
  title = {Parametricity and dependent types},
  author = {Jean-Philippe Bernardy and Patrik Jansson and Ross Paterson},
  year = {2010},
  doi = {10.1145/1863543.1863592},
  url = {http://doi.acm.org/10.1145/1863543.1863592},
  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 = {Paul Hudak and Stephanie Weirich},
  publisher = {ACM},
  isbn = {978-1-60558-794-3},
}

@inproceedings{Norell13,
  title = {Interactive programming with dependent types},
  author = {Ulf Norell},
  year = {2013},
  doi = {10.1145/2500365.2500610},
  url = {http://doi.acm.org/10.1145/2500365.2500610},
  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 = {Greg Morrisett and Tarmo Uustalu},
  publisher = {ACM},
  isbn = {978-1-4503-2326-0},
}

@inproceedings{LicataB15,
  title = {A Cubical Approach to Synthetic Homotopy Theory},
  author = {Daniel R. Licata and Guillaume Brunerie},
  year = {2015},
  doi = {10.1109/LICS.2015.19},
  url = {http://dx.doi.org/10.1109/LICS.2015.19},
  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},
}

@inproceedings{OrtonP17-0,
  title = {Decomposing the Univalence Axiom},
  author = {Ian Orton and Andrew M. Pitts},
  year = {2017},
  doi = {10.4230/LIPIcs.TYPES.2017.6},
  url = {https://doi.org/10.4230/LIPIcs.TYPES.2017.6},
  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 = {Andreas Abel 0001 and Fredrik Nordvall Forsberg and Ambrus Kaposi},
  volume = {104},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-95977-071-2},
}

@article{Escardo13-1,
  title = {Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics},
  author = {Martín Escardó},
  year = {2013},
  url = {http://projecteuclid.org/euclid.jsl/1389032274},
  researchr = {https://researchr.org/publication/Escardo13-1},
  cites = {0},
  citedby = {0},
  journal = {Journal of Symbolic Logic},
  volume = {78},
  number = {3},
  pages = {764-784},
}

@inproceedings{Jeffrey14,
  title = {Functional reactive types},
  author = {Alan Jeffrey},
  year = {2014},
  doi = {10.1145/2603088.2603106},
  url = {http://doi.acm.org/10.1145/2603088.2603106},
  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 = {Thomas A. Henzinger and Dale Miller},
  publisher = {ACM},
  isbn = {978-1-4503-2886-9},
}

@article{FeitosaRB21,
  title = {Towards an Extrinsic Formalization of Featherweight Java in Agda},
  author = {Samuel da Silva Feitosa and Rodrigo Geraldo Ribeiro and André Rauber Du Bois},
  year = {2021},
  doi = {10.19153/cleiej.24.3.3},
  url = {https://doi.org/10.19153/cleiej.24.3.3},
  researchr = {https://researchr.org/publication/FeitosaRB21},
  cites = {0},
  citedby = {0},
  journal = {CLEI Electron. J.},
  volume = {24},
  number = {3},
}

@inproceedings{KoG13-1,
  title = {Relational algebraic ornaments},
  author = {Hsiang-Shang Ko and Jeremy Gibbons},
  year = {2013},
  doi = {10.1145/2502409.2502413},
  url = {http://doi.acm.org/10.1145/2502409.2502413},
  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 = {Stephanie Weirich},
  publisher = {ACM},
  isbn = {978-1-4503-2384-0},
}

@inproceedings{SchwaabS13,
  title = {Modular type-safety proofs in Agda},
  author = {Christopher Schwaab and Jeremy G. Siek},
  year = {2013},
  doi = {10.1145/2428116.2428120},
  url = {http://doi.acm.org/10.1145/2428116.2428120},
  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 = {Matthew Might and David Van Horn and Andreas Abel 0001 and Tim Sheard},
  publisher = {ACM},
  isbn = {978-1-4503-1860-0},
}

@inproceedings{Vivekanandan18-0,
  title = {Code Generation for Higher Inductive Types - A Study in Agda Metaprogramming},
  author = {Paventhan Vivekanandan},
  year = {2018},
  doi = {10.1007/978-3-030-16202-3_2},
  url = {https://doi.org/10.1007/978-3-030-16202-3_2},
  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 = {Josep Silva},
  volume = {11285},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-16202-3},
}

@article{DaggittZG20,
  title = {A Relaxation of Üresin and Dubois' Asynchronous Fixed-Point Theory in Agda},
  author = {Matthew L. Daggitt and Ran Zmigrod and Timothy G. Griffin},
  year = {2020},
  doi = {10.1007/s10817-019-09536-w},
  url = {https://doi.org/10.1007/s10817-019-09536-w},
  researchr = {https://researchr.org/publication/DaggittZG20},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {64},
  number = {5},
  pages = {857-877},
}

@article{ValliappanRC22,
  title = {Normalization for fitch-style modal calculi},
  author = {Nachiappan Valliappan and Fabian Ruch and Carlos Tomé Cortiñas},
  year = {2022},
  doi = {10.1145/3547649},
  url = {https://doi.org/10.1145/3547649},
  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},
}

@inproceedings{McBride14-2,
  title = {How to keep your neighbours in order},
  author = {Conor Thomas McBride},
  year = {2014},
  doi = {10.1145/2628136.2628163},
  url = {http://doi.acm.org/10.1145/2628136.2628163},
  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 = {Johan Jeuring and Manuel M. T. Chakravarty},
  publisher = {ACM},
  isbn = {978-1-4503-2873-9},
}

@inproceedings{Pouillard11,
  title = {Nameless, painless},
  author = {Nicolas Pouillard},
  year = {2011},
  doi = {10.1145/2034773.2034817},
  url = {http://doi.acm.org/10.1145/2034773.2034817},
  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 = {Manuel M. T. Chakravarty and Zhenjiang Hu and Olivier Danvy},
  publisher = {ACM},
  isbn = {978-1-4503-0865-6},
}

@article{GilbertCST19,
  title = {Definitional proof-irrelevance without K},
  author = {Gaëtan Gilbert and Jesper Cockx and Matthieu Sozeau and Nicolas Tabareau},
  year = {2019},
  url = {https://dl.acm.org/citation.cfm?id=3290316},
  researchr = {https://researchr.org/publication/GilbertCST19},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
}

@misc{https:-doi.org-10.48550-arxiv.2103.09092,
  title = {The Agda Universal Algebra Library, Part 2: Structure},
  author = {DeMeo, William},
  year = {2021},
  doi = {10.48550/ARXIV.2103.09092},
  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},
}

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

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

@article{KoCL22-0,
  title = {Datatype-generic programming meets elaborator reflection},
  author = {Hsiang-Shang Ko and Liang-Ting Chen and Tzu-Chi Lin},
  year = {2022},
  doi = {10.1145/3547629},
  url = {https://doi.org/10.1145/3547629},
  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},
}

@inproceedings{MuKJ08,
  title = {Algebra of Programming Using Dependent Types},
  author = {Shin-Cheng Mu and Hsiang-Shang Ko and Patrik Jansson},
  year = {2008},
  doi = {10.1007/978-3-540-70594-9_15},
  url = {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 = {Philippe Audebaud and Christine Paulin-Mohring},
  volume = {5133},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-70593-2},
}

@article{MaarandU19,
  title = {Certified normalization of generalized traces},
  author = {Hendrik Maarand and Tarmo Uustalu},
  year = {2019},
  doi = {10.1007/s11334-019-00347-1},
  url = {https://doi.org/10.1007/s11334-019-00347-1},
  researchr = {https://researchr.org/publication/MaarandU19},
  cites = {0},
  citedby = {0},
  journal = {ISSE},
  volume = {15},
  number = {3-4},
  pages = {253-265},
}

@article{DagandM14,
  title = {Transporting functions across ornaments},
  author = {Pierre-Évariste Dagand and Conor McBride},
  year = {2014},
  doi = {10.1017/S0956796814000069},
  url = {http://dx.doi.org/10.1017/S0956796814000069},
  researchr = {https://researchr.org/publication/DagandM14},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {24},
  number = {2-3},
  pages = {316-383},
}

@inproceedings{XuE13-1,
  title = {A Constructive Model of Uniform Continuity},
  author = {Chuangjie Xu and Martín Hötzel Escardó},
  year = {2013},
  doi = {10.1007/978-3-642-38946-7_18},
  url = {http://dx.doi.org/10.1007/978-3-642-38946-7_18},
  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 = {Masahito Hasegawa},
  volume = {7941},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-38946-7},
}

@inproceedings{CarrJMMS22,
  title = {Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda},
  author = {Harold Carr and Christa Jenkins and Mark Moir and Victor Cacciari Miraldo and Lisandra Silva},
  year = {2022},
  doi = {10.1007/978-3-031-06773-0_33},
  url = {https://doi.org/10.1007/978-3-031-06773-0_33},
  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 = {Jyotirmoy V. Deshmukh and Klaus Havelund and Ivan Perez 0001},
  volume = {13260},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-031-06773-0},
}

@article{RouvoetKV21,
  title = {Intrinsically typed compilation with nameless labels},
  author = {Arjen Rouvoet and Robbert Krebbers and Eelco Visser},
  year = {2021},
  doi = {10.1145/3434303},
  url = {https://doi.org/10.1145/3434303},
  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},
}

@inproceedings{FirsovU15,
  title = {Certified Normalization of Context-Free Grammars},
  author = {Denis Firsov and Tarmo Uustalu},
  year = {2015},
  doi = {10.1145/2676724.2693177},
  url = {http://doi.acm.org/10.1145/2676724.2693177},
  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 = {Xavier Leroy and Alwen Tiu},
  publisher = {ACM},
  isbn = {978-1-4503-3296-5},
}

@article{CockxTW21,
  title = {The taming of the rew: a type theory with computational assumptions},
  author = {Jesper Cockx and Nicolas Tabareau and Théo Winterhalter},
  year = {2021},
  doi = {10.1145/3434341},
  url = {https://doi.org/10.1145/3434341},
  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},
}

@article{DaraisH19,
  title = {Constructive Galois Connections},
  author = {David Darais and David Van Horn},
  year = {2019},
  doi = {10.1017/S0956796819000066},
  url = {https://doi.org/10.1017/S0956796819000066},
  researchr = {https://researchr.org/publication/DaraisH19},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {29},
}

@inproceedings{Kahl11-0,
  title = {Dependently-Typed Formalisation of Relation-Algebraic Abstractions},
  author = {Wolfram Kahl},
  year = {2011},
  doi = {10.1007/978-3-642-21070-9_18},
  url = {http://dx.doi.org/10.1007/978-3-642-21070-9_18},
  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 = {Harrie C. M. de Swart},
  volume = {6663},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-21069-3},
}

@article{NiuSGH22,
  title = {A cost-aware logical framework},
  author = {Yue Niu and Jonathan Sterling and Harrison Grodin and Robert Harper},
  year = {2022},
  doi = {10.1145/3498670},
  url = {https://doi.org/10.1145/3498670},
  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},
}

@article{KinoshitaP14,
  title = {Category theoretic structure of setoids},
  author = {Yoshiki Kinoshita and John Power},
  year = {2014},
  doi = {10.1016/j.tcs.2014.03.006},
  url = {http://dx.doi.org/10.1016/j.tcs.2014.03.006},
  researchr = {https://researchr.org/publication/KinoshitaP14},
  cites = {0},
  citedby = {0},
  journal = {Theoretical Computer Science},
  volume = {546},
  pages = {145-163},
}

@inproceedings{LohM11,
  title = {Generic programming with indexed functors},
  author = {Andres Löh and José Pedro Magalhães},
  year = {2011},
  doi = {10.1145/2036918.2036920},
  url = {http://doi.acm.org/10.1145/2036918.2036920},
  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 = {Jaakko Järvi and Shin-Cheng Mu},
  publisher = {ACM},
  isbn = {978-1-4503-0861-8},
}

@inproceedings{Danielsson13,
  title = {Correct-by-construction pretty-printing},
  author = {Nils Anders Danielsson},
  year = {2013},
  doi = {10.1145/2502409.2502410},
  url = {http://doi.acm.org/10.1145/2502409.2502410},
  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 = {Stephanie Weirich},
  publisher = {ACM},
  isbn = {978-1-4503-2384-0},
}

@article{Swierstra10,
  title = {More dependent types for distributed arrays},
  author = {Wouter Swierstra},
  year = {2010},
  doi = {10.1007/s10990-011-9075-y},
  url = {http://dx.doi.org/10.1007/s10990-011-9075-y},
  researchr = {https://researchr.org/publication/Swierstra10},
  cites = {0},
  citedby = {0},
  journal = {Higher-Order and Symbolic Computation},
  volume = {23},
  number = {4},
  pages = {489-506},
}

@inproceedings{McBride10-2,
  title = {Djinn, Monotonic},
  author = {Conor McBride},
  year = {2010},
  url = {http://www.easychair.org/publications/?page=711183398},
  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 = {Ekaterina Komendantskaya and Ana Bove and Milad Niqui},
  volume = {5},
  series = {EPiC Series},
  publisher = {EasyChair},
}

@inproceedings{ZalakainD21,
  title = {π with Leftovers: A Mechanisation in Agda},
  author = {Uma Zalakain and Ornela Dardha},
  year = {2021},
  doi = {10.1007/978-3-030-78089-0_9},
  url = {https://doi.org/10.1007/978-3-030-78089-0_9},
  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 = {Kirstin Peters and Tim A. C. Willemse},
  volume = {12719},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-78089-0},
}

@article{PujetT22,
  title = {Observational equality: now for good},
  author = {Loïc Pujet and Nicolas Tabareau},
  year = {2022},
  doi = {10.1145/3498693},
  url = {https://doi.org/10.1145/3498693},
  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},
}

@inproceedings{MorgensternL10,
  title = {Security-typed programming within dependently typed programming},
  author = {Jamie Morgenstern and Daniel R. Licata},
  year = {2010},
  doi = {10.1145/1863543.1863569},
  url = {http://doi.acm.org/10.1145/1863543.1863569},
  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 = {Paul Hudak and Stephanie Weirich},
  publisher = {ACM},
  isbn = {978-1-60558-794-3},
}

@article{HancockH06,
  title = {Programming interfaces and basic topology},
  author = {Peter Hancock and Pierre Hyvernat},
  year = {2006},
  doi = {10.1016/j.apal.2005.05.022},
  url = {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},
}

@article{PickardH21,
  title = {Calculating dependently-typed compilers (functional pearl)},
  author = {Mitchell Pickard and Graham Hutton},
  year = {2021},
  doi = {10.1145/3473587},
  url = {https://doi.org/10.1145/3473587},
  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},
}

@inproceedings{DevrieseP13,
  title = {Typed syntactic meta-programming},
  author = {Dominique Devriese and Frank Piessens},
  year = {2013},
  doi = {10.1145/2500365.2500575},
  url = {http://doi.acm.org/10.1145/2500365.2500575},
  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 = {Greg Morrisett and Tarmo Uustalu},
  publisher = {ACM},
  isbn = {978-1-4503-2326-0},
}

@article{PoulsenRTKV18,
  title = {Intrinsically-typed definitional interpreters for imperative languages},
  author = {Casper Bach Poulsen and Arjen Rouvoet and Andrew P. Tolmach and Robbert Krebbers and Eelco Visser},
  year = {2018},
  doi = {10.1145/3158104},
  url = {http://doi.acm.org/10.1145/3158104},
  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},
}

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

@inproceedings{FosterS11-0,
  title = {Integrating an Automated Theorem Prover into Agda},
  author = {Simon Foster and Georg Struth},
  year = {2011},
  doi = {10.1007/978-3-642-20398-5_10},
  url = {http://dx.doi.org/10.1007/978-3-642-20398-5_10},
  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 = {Mihaela Gheorghiu Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi},
  volume = {6617},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-20397-8},
}

@inproceedings{FlorSS15,
  title = {Pi-Ware: Hardware Description and Verification in Agda},
  author = {João Paulo Pizani Flor and Wouter Swierstra and Yorick Sijsling},
  year = {2015},
  doi = {10.4230/LIPIcs.TYPES.2015.9},
  url = {https://doi.org/10.4230/LIPIcs.TYPES.2015.9},
  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 = {Tarmo Uustalu},
  volume = {69},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-95977-030-9},
}

@phdthesis{basesearch-7836,
  title = {Dependent Pattern Matching and Proof-Relevant Unification},
  author = {Jesper Cockx},
  year = {2017},
  url = {https://www.base-search.net/Record/66a7ce9719c00dd2b976ac2c0f472c9fa527c0fcc5fbe259b2c5ca71b4f5ecc7},
  note = {base-search.net (ftunivleuven:oai:lirias.kuleuven.be:123456789/583556)},
  researchr = {https://researchr.org/publication/basesearch-7836},
  cites = {0},
  citedby = {0},
  school = {Katholieke Universiteit Leuven, Belgium},
}

@inproceedings{Prieto-Cubides22,
  title = {On homotopy of walks and spherical maps in homotopy type theory},
  author = {Jonathan Prieto-Cubides},
  year = {2022},
  doi = {10.1145/3497775.3503671},
  url = {https://doi.org/10.1145/3497775.3503671},
  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 = {Andrei Popescu 0001 and Steve Zdancewic},
  publisher = {ACM},
  isbn = {978-1-4503-9182-5},
}

@inproceedings{AltenkirchD10,
  title = {Termination Checking in the Presence of Nested Inductive and Coinductive Types},
  author = {Thorsten Altenkirch and Nils Anders Danielsson},
  year = {2010},
  url = {http://www.easychair.org/publications/?page=751599912},
  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 = {Ekaterina Komendantskaya and Ana Bove and Milad Niqui},
  volume = {5},
  series = {EPiC Series},
  publisher = {EasyChair},
}

@inproceedings{CaretteS16-0,
  title = {Computing with Semirings and Weak Rig Groupoids},
  author = {Jacques Carette and Amr Sabry},
  year = {2016},
  doi = {10.1007/978-3-662-49498-1_6},
  url = {http://dx.doi.org/10.1007/978-3-662-49498-1_6},
  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 = {Peter Thiemann},
  volume = {9632},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-662-49497-4},
}

@inproceedings{SinkarovsC21,
  title = {Extracting the power of dependent types},
  author = {Artjoms Sinkarovs and Jesper Cockx},
  year = {2021},
  doi = {10.1145/3486609.3487201},
  url = {https://doi.org/10.1145/3486609.3487201},
  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 = {Eli Tilevich and Coen De Roover},
  publisher = {ACM},
  isbn = {978-1-4503-9112-2},
}

@inproceedings{HancockMGMA13,
  title = {Small Induction Recursion},
  author = {Peter Hancock and Conor McBride and Neil Ghani and Lorenzo Malatesta and Thorsten Altenkirch},
  year = {2013},
  doi = {10.1007/978-3-642-38946-7_13},
  url = {http://dx.doi.org/10.1007/978-3-642-38946-7_13},
  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 = {Masahito Hasegawa},
  volume = {7941},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-38946-7},
}

@inproceedings{CockxD17,
  title = {Lifting proof-relevant unification to higher dimensions},
  author = {Jesper Cockx and Dominique Devriese},
  year = {2017},
  doi = {10.1145/3018610.3018612},
  url = {http://doi.acm.org/10.1145/3018610.3018612},
  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 = {Yves Bertot and Viktor Vafeiadis},
  publisher = {ACM},
  isbn = {978-1-4503-4705-1},
}

@article{ChiangM16,
  title = {Formal derivation of Greedy algorithms from relational specifications: A tutorial},
  author = {Yu-Hsi Chiang and Shin-Cheng Mu},
  year = {2016},
  doi = {10.1016/j.jlamp.2015.12.003},
  url = {http://dx.doi.org/10.1016/j.jlamp.2015.12.003},
  researchr = {https://researchr.org/publication/ChiangM16},
  cites = {0},
  citedby = {0},
  journal = {Journal of Logic and Algebraic Programming},
  volume = {85},
  number = {5},
  pages = {879-905},
}

@article{CockxDP16-0,
  title = {Eliminating dependent pattern matching without K},
  author = {Jesper Cockx and Dominique Devriese and Frank Piessens},
  year = {2016},
  doi = {10.1017/S0956796816000174},
  url = {http://dx.doi.org/10.1017/S0956796816000174},
  researchr = {https://researchr.org/publication/CockxDP16-0},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {26},
}

@inproceedings{LLL09diff,
  title = {Type-safe diff for families of datatypes},
  author = {Eelco Lempsink and Sean Leather and Andres Löh},
  year = {2009},
  doi = {10.1145/1596614.1596624},
  url = {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},
}

@inproceedings{CortinasS18,
  title = {From algebra to abstract machine: a verified generic construction},
  author = {Carlos Tomé Cortiñas and Wouter Swierstra},
  year = {2018},
  doi = {10.1145/3240719.3241787},
  url = {https://doi.org/10.1145/3240719.3241787},
  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 = {Richard A. Eisenberg and Niki Vazou},
  publisher = {ACM},
}

@inproceedings{FredrikssonG14-0,
  title = {Krivine nets: a semantic foundation for distributed execution},
  author = {Olle Fredriksson and Dan R. Ghica},
  year = {2014},
  doi = {10.1145/2628136.2628152},
  url = {http://doi.acm.org/10.1145/2628136.2628152},
  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 = {Johan Jeuring and Manuel M. T. Chakravarty},
  publisher = {ACM},
  isbn = {978-1-4503-2873-9},
}

@article{VezzosiM019,
  title = {Cubical agda: a dependently typed programming language with univalence and higher inductive types},
  author = {Andrea Vezzosi and Anders Mörtberg and Andreas Abel},
  year = {2019},
  doi = {10.1145/3341691},
  url = {https://doi.org/10.1145/3341691},
  researchr = {https://researchr.org/publication/VezzosiM019},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
}

@article{Escardo13-0,
  title = {Continuity of Gödel's System T Definable Functionals via Effectful Forcing},
  author = {Martín Hötzel Escardó},
  year = {2013},
  doi = {10.1016/j.entcs.2013.09.010},
  url = {http://dx.doi.org/10.1016/j.entcs.2013.09.010},
  researchr = {https://researchr.org/publication/Escardo13-0},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {298},
  pages = {119-141},
}

@article{FirsovU14,
  title = {Certified CYK parsing of context-free languages},
  author = {Denis Firsov and Tarmo Uustalu},
  year = {2014},
  doi = {10.1016/j.jlamp.2014.09.002},
  url = {http://dx.doi.org/10.1016/j.jlamp.2014.09.002},
  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},
}

@article{Calderon18,
  title = {Formalizing Constructive Projective Geometry in Agda},
  author = {Guillermo Calderón},
  year = {2018},
  doi = {10.1016/j.entcs.2018.10.005},
  url = {https://doi.org/10.1016/j.entcs.2018.10.005},
  researchr = {https://researchr.org/publication/Calderon18},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {338},
  pages = {61-77},
}

@misc{https:-doi.org-10.48550-arxiv.2205.08354,
  title = {Constructive Analysis in the Agda Proof Assistant},
  author = {Murray, Zachary},
  year = {2022},
  doi = {10.48550/ARXIV.2205.08354},
  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},
}

@article{VezzosiMA21,
  title = {Cubical Agda: A dependently typed programming language with univalence and higher inductive types},
  author = {Andrea Vezzosi and Anders Mörtberg and Andreas Abel 0001},
  year = {2021},
  doi = {10.1017/S0956796821000034},
  url = {https://doi.org/10.1017/S0956796821000034},
  researchr = {https://researchr.org/publication/VezzosiMA21},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {31},
}

@inproceedings{BoveDS12,
  title = {Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs},
  author = {Ana Bove and Peter Dybjer and Andrés Sicard-Ramírez},
  year = {2012},
  doi = {10.1007/978-3-642-28729-9_7},
  url = {http://dx.doi.org/10.1007/978-3-642-28729-9_7},
  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 = {Lars Birkedal},
  volume = {7213},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-28728-2},
}

@inproceedings{Jeffrey13-0,
  title = {Causality for free!: parametricity implies causality for functional reactive programs},
  author = {Alan Jeffrey},
  year = {2013},
  doi = {10.1145/2428116.2428127},
  url = {http://doi.acm.org/10.1145/2428116.2428127},
  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 = {Matthew Might and David Van Horn and Andreas Abel 0001 and Tim Sheard},
  publisher = {ACM},
  isbn = {978-1-4503-1860-0},
}

@inproceedings{BrunerieLM22,
  title = {Synthetic Integral Cohomology in Cubical Agda},
  author = {Guillaume Brunerie and Axel Ljungström and Anders Mörtberg},
  year = {2022},
  doi = {10.4230/LIPIcs.CSL.2022.11},
  url = {https://doi.org/10.4230/LIPIcs.CSL.2022.11},
  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 = {Florin Manea and Alex Simpson},
  volume = {216},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-218-1},
}

@inproceedings{Genestier20,
  title = {Encoding Agda Programs Using Rewriting},
  author = {Guillaume Genestier},
  year = {2020},
  doi = {10.4230/LIPIcs.FSCD.2020.31},
  url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.31},
  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 = {Zena M. Ariola},
  volume = {167},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-155-9},
}

@article{PouillardP12,
  title = {A unified treatment of syntax with binders},
  author = {Nicolas Pouillard and François Pottier},
  year = {2012},
  doi = {10.1017/S0956796812000251},
  url = {http://dx.doi.org/10.1017/S0956796812000251},
  researchr = {https://researchr.org/publication/PouillardP12},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {22},
  number = {4-5},
  pages = {614-704},
}

@inproceedings{AngiuliMLH14,
  title = {Homotopical patch theory},
  author = {Carlo Angiuli and Edward Morehouse and Daniel R. Licata and Robert Harper},
  year = {2014},
  doi = {10.1145/2628136.2628158},
  url = {http://doi.acm.org/10.1145/2628136.2628158},
  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 = {Johan Jeuring and Manuel M. T. Chakravarty},
  publisher = {ACM},
  isbn = {978-1-4503-2873-9},
}

@inproceedings{VeltriV20,
  title = {Formalizing π-calculus in guarded cubical Agda},
  author = {Niccolò Veltri and Andrea Vezzosi},
  year = {2020},
  doi = {10.1145/3372885.3373814},
  url = {https://doi.org/10.1145/3372885.3373814},
  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 = {Jasmin Blanchette and Catalin Hritcu},
  publisher = {ACM},
  isbn = {978-1-4503-7097-4},
}

@article{UustaluV17,
  title = {Finiteness and rational sequences, constructively},
  author = {Tarmo Uustalu and Niccolò Veltri},
  year = {2017},
  doi = {10.1017/S0956796817000041},
  url = {http://dx.doi.org/10.1017/S0956796817000041},
  researchr = {https://researchr.org/publication/UustaluV17},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {27},
}

@inproceedings{DiehlS13,
  title = {Leveling up dependent types: generic programming over a predicative hierarchy of universes},
  author = {Larry Diehl and Tim Sheard},
  year = {2013},
  doi = {10.1145/2502409.2502414},
  url = {http://doi.acm.org/10.1145/2502409.2502414},
  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 = {Stephanie Weirich},
  publisher = {ACM},
  isbn = {978-1-4503-2384-0},
}

@article{OmarVCH19,
  title = {Live functional programming with typed holes},
  author = {Cyrus Omar and Ian Voysey and Ravi Chugh and Matthew A. Hammer},
  year = {2019},
  url = {https://dl.acm.org/citation.cfm?id=3290327},
  researchr = {https://researchr.org/publication/OmarVCH19},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
}

@inproceedings{LicataH09,
  title = {A universe of binding and computation},
  author = {Daniel R. Licata and Robert Harper},
  year = {2009},
  doi = {10.1145/1596550.1596571},
  url = {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 = {Graham Hutton and Andrew P. Tolmach},
  publisher = {ACM},
  isbn = {978-1-60558-332-7},
}

@article{ChapmanUV17,
  title = {Formalizing Restriction Categories},
  author = {James Chapman and Tarmo Uustalu and Niccolò Veltri},
  year = {2017},
  doi = {10.6092/issn.1972-5787/6237},
  url = {https://doi.org/10.6092/issn.1972-5787/6237},
  researchr = {https://researchr.org/publication/ChapmanUV17},
  cites = {0},
  citedby = {0},
  journal = {J. Formalized Reasoning},
  volume = {10},
  number = {1},
  pages = {1-36},
}

@inproceedings{9640056,
  title = {Formalizing Affinization of a Projective Plane in Agda},
  author = {Calderón, 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)},
}

@inproceedings{KellerA10,
  title = {Hereditary Substitutions for Simple Types, Formalized},
  author = {Chantal Keller and Thorsten Altenkirch},
  year = {2010},
  doi = {10.1145/1863597.1863601},
  url = {http://doi.acm.org/10.1145/1863597.1863601},
  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 = {Venanzio Capretta and James Chapman 0001},
  publisher = {ACM},
  isbn = {978-1-4503-0255-5},
}

@inproceedings{CopelloTB14,
  title = {Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda},
  author = {Ernesto Copello and Alvaro Tasistro and Bruno Bianchi},
  year = {2014},
  doi = {10.1007/978-3-319-11863-5_5},
  url = {http://dx.doi.org/10.1007/978-3-319-11863-5_5},
  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 = {Fernando Magno Quintão Pereira},
  volume = {8771},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-11862-8},
}

@inproceedings{ForsbergS10,
  title = {Inductive-Inductive Definitions},
  author = {Fredrik Nordvall Forsberg and Anton Setzer},
  year = {2010},
  doi = {10.1007/978-3-642-15205-4_35},
  url = {http://dx.doi.org/10.1007/978-3-642-15205-4_35},
  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 = {Anuj Dawar and Helmut Veith},
  volume = {6247},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-15204-7},
}

@inproceedings{Wadler18,
  title = {Programming Language Foundations in Agda},
  author = {Philip Wadler},
  year = {2018},
  doi = {10.1007/978-3-030-03044-5_5},
  url = {https://doi.org/10.1007/978-3-030-03044-5_5},
  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 = {Tiago Massoni and Mohammad Reza Mousavi},
  volume = {11254},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-03044-5},
}

@inproceedings{WinantCD17,
  title = {Expressive and strongly type-safe code generation},
  author = {Thomas Winant and Jesper Cockx and Dominique Devriese},
  year = {2017},
  doi = {10.1145/3131851.3131872},
  url = {http://doi.acm.org/10.1145/3131851.3131872},
  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 = {Wim Vanhoof and Brigitte Pientka},
  publisher = {ACM},
  isbn = {978-1-4503-5291-8},
}

@article{TasistroCS15,
  title = {Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda Calculus},
  author = {Alvaro Tasistro and Ernesto Copello and Nora Szasz},
  year = {2015},
  doi = {10.1016/j.entcs.2015.04.013},
  url = {http://dx.doi.org/10.1016/j.entcs.2015.04.013},
  researchr = {https://researchr.org/publication/TasistroCS15},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {312},
  pages = {215-230},
}

@article{0001VW17,
  title = {Normalization by evaluation for sized dependent types},
  author = {Andreas Abel and Andrea Vezzosi and Théo Winterhalter},
  year = {2017},
  doi = {10.1145/3110277},
  url = {http://doi.acm.org/10.1145/3110277},
  researchr = {https://researchr.org/publication/0001VW17},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {1},
  number = {ICFP},
}

@inproceedings{CaiGRO14,
  title = {A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation},
  author = {Yufei Cai and Paolo G. Giarrusso and Tillmann Rendel and Klaus Ostermann},
  year = {2014},
  doi = {10.1145/2594291.2594304},
  url = {http://doi.acm.org/10.1145/2594291.2594304},
  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 = {Michael F. P. O'Boyle and Keshav Pingali},
  publisher = {ACM},
  isbn = {978-1-4503-2784-8},
}

@inproceedings{KrausECA13,
  title = {Generalizations of Hedberg's Theorem},
  author = {Nicolai Kraus and Martín Hötzel Escardó and Thierry Coquand and Thorsten Altenkirch},
  year = {2013},
  doi = {10.1007/978-3-642-38946-7_14},
  url = {http://dx.doi.org/10.1007/978-3-642-38946-7_14},
  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 = {Masahito Hasegawa},
  volume = {7941},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-38946-7},
}

@phdthesis{ethos-10479,
  title = {Truncation levels in homotopy type theory},
  author = {Nicolai Kraus},
  year = {2015},
  url = {http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.668635},
  note = {British Library, EThOS},
  researchr = {https://researchr.org/publication/ethos-10479},
  cites = {0},
  citedby = {0},
  school = {University of Nottingham, UK},
}

@inproceedings{DeMeoC21,
  title = {A Machine-Checked Proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory},
  author = {William J. DeMeo and Jacques Carette},
  year = {2021},
  doi = {10.4230/LIPIcs.TYPES.2021.4},
  url = {https://doi.org/10.4230/LIPIcs.TYPES.2021.4},
  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 = {Henning Basold and Jesper Cockx and Silvia Ghilezan},
  volume = {239},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-254-9},
}

@inproceedings{AltenkirchMS07,
  title = {Observational equality, now!},
  author = {Thorsten Altenkirch and Conor McBride and Wouter Swierstra},
  year = {2007},
  doi = {10.1145/1292597.1292608},
  url = {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 = {Aaron Stump and Hongwei Xi},
  publisher = {ACM},
  isbn = {978-1-59593-677-6},
}

@inproceedings{ThiemannC12,
  title = {Agda Meets Accelerate},
  author = {Peter Thiemann and Manuel M. T. Chakravarty},
  year = {2012},
  doi = {10.1007/978-3-642-41582-1_11},
  url = {http://dx.doi.org/10.1007/978-3-642-41582-1_11},
  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 = {Ralf Hinze},
  volume = {8241},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-41581-4},
}

@inproceedings{AlhabardiBLS21,
  title = {Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control},
  author = {Fahad F. Alhabardi and Arnold Beckmann and Bogdan Lazar and Anton Setzer},
  year = {2021},
  doi = {10.4230/LIPIcs.TYPES.2021.1},
  url = {https://doi.org/10.4230/LIPIcs.TYPES.2021.1},
  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 = {Henning Basold and Jesper Cockx and Silvia Ghilezan},
  volume = {239},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-254-9},
}

@inproceedings{Danielsson06,
  title = {A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family},
  author = {Nils Anders Danielsson},
  year = {2006},
  doi = {10.1007/978-3-540-74464-1_7},
  url = {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 = {Thorsten Altenkirch and Conor McBride},
  volume = {4502},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-74463-4},
}

@inproceedings{UustaluV17-1,
  title = {Partiality and Container Monads},
  author = {Tarmo Uustalu and Niccolò Veltri},
  year = {2017},
  doi = {10.1007/978-3-319-71237-6_20},
  url = {https://doi.org/10.1007/978-3-319-71237-6_20},
  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 = {Bor-Yuh Evan Chang},
  volume = {10695},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-71237-6},
}

@inproceedings{DaggittGG18,
  title = {Asynchronous convergence of policy-rich distributed bellman-ford routing protocols},
  author = {Matthew L. Daggitt and Alexander J. T. Gurney and Timothy G. Griffin},
  year = {2018},
  doi = {10.1145/3230543.3230561},
  url = {https://doi.org/10.1145/3230543.3230561},
  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 = {Sergey Gorinsky and János Tapolcai},
  publisher = {ACM},
}

@inproceedings{OConnor16-0,
  title = {Applications of applicative proof search},
  author = {Liam O'Connor},
  year = {2016},
  doi = {10.1145/2976022.2976030},
  url = {http://doi.acm.org/10.1145/2976022.2976030},
  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 = {James Chapman and Wouter Swierstra},
  publisher = {ACM},
  isbn = {978-1-4503-4435-7},
}

@inproceedings{McBride12-0,
  title = {Agda-curious?: an exploration of programming with dependent types},
  author = {Conor Thomas McBride},
  year = {2012},
  doi = {10.1145/2364527.2364529},
  url = {http://doi.acm.org/10.1145/2364527.2364529},
  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 = {Peter Thiemann and Robby Bruce Findler},
  publisher = {ACM},
  isbn = {978-1-4503-1054-3},
}

@article{KrausS15,
  title = {Higher Homotopies in a Hierarchy of Univalent Universes},
  author = {Nicolai Kraus and Christian Sattler},
  year = {2015},
  doi = {10.1145/2729979},
  url = {http://doi.acm.org/10.1145/2729979},
  researchr = {https://researchr.org/publication/KrausS15},
  cites = {0},
  citedby = {0},
  journal = {ACM Trans. Comput. Log.},
  volume = {16},
  number = {2},
  pages = {18},
}

@inproceedings{LicataF14-0,
  title = {Eilenberg-MacLane spaces in homotopy type theory},
  author = {Daniel R. Licata and Eric Finster},
  year = {2014},
  doi = {10.1145/2603088.2603153},
  url = {http://doi.acm.org/10.1145/2603088.2603153},
  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 = {Thomas A. Henzinger and Dale Miller},
  publisher = {ACM},
  isbn = {978-1-4503-2886-9},
}

@inproceedings{DiehlS14,
  title = {Generic constructors and eliminators from descriptions: type theory as a dependently typed internal DSL},
  author = {Larry Diehl and Tim Sheard},
  year = {2014},
  doi = {10.1145/2633628.2633630},
  url = {http://doi.acm.org/10.1145/2633628.2633630},
  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 = {José Pedro Magalháes and Tiark Rompf},
  publisher = {ACM},
  isbn = {978-1-4503-3042-8},
}

@article{AltenkirchCU14,
  title = {Relative Monads Formalised},
  author = {Thorsten Altenkirch and James Chapman and Tarmo Uustalu},
  year = {2014},
  doi = {10.6092/issn.1972-5787/4389},
  url = {http://dx.doi.org/10.6092/issn.1972-5787/4389},
  researchr = {https://researchr.org/publication/AltenkirchCU14},
  cites = {0},
  citedby = {0},
  journal = {J. Formalized Reasoning},
  volume = {7},
  number = {1},
  pages = {1-43},
}

@inproceedings{UustaluV17-0,
  title = {The Delay Monad and Restriction Categories},
  author = {Tarmo Uustalu and Niccolò Veltri},
  year = {2017},
  doi = {10.1007/978-3-319-67729-3_3},
  url = {https://doi.org/10.1007/978-3-319-67729-3_3},
  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 = {Dang Van Hung and Deepak Kapur},
  volume = {10580},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-67729-3},
}

@inproceedings{AhrensCS15,
  title = {Non-Wellfounded Trees in Homotopy Type Theory},
  author = {Benedikt Ahrens and Paolo Capriotti and Régis Spadotti},
  year = {2015},
  doi = {10.4230/LIPIcs.TLCA.2015.17},
  url = {http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.17},
  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 = {Thorsten Altenkirch},
  volume = {38},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-939897-87-3},
}

@inproceedings{ManzinoP20,
  title = {Agda Formalization of a Security-preserving Translation from Flow-sensitive to Flow-insensitive Security Types},
  author = {Cecilia Manzino and Alberto Pardo},
  year = {2020},
  doi = {10.1016/j.entcs.2020.08.005},
  url = {https://doi.org/10.1016/j.entcs.2020.08.005},
  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 = {Cláudia Nalon},
  volume = {351},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier},
}

@article{FlorenceYTF19,
  title = {A calculus for Esterel: if can, can. if no can, no can},
  author = {Spencer P. Florence and Shu-Hung You and Jesse A. Tov and Robert Bruce Findler},
  year = {2019},
  url = {https://dl.acm.org/citation.cfm?id=3290374},
  researchr = {https://researchr.org/publication/FlorenceYTF19},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
}

@inproceedings{OuryS08,
  title = {The power of Pi},
  author = {Nicolas Oury and Wouter Swierstra},
  year = {2008},
  doi = {10.1145/1411204.1411213},
  url = {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 = {James Hook and Peter Thiemann},
  publisher = {ACM},
  isbn = {978-1-59593-919-7},
}

@article{FioreS22,
  title = {Formal metatheory of second-order abstract syntax},
  author = {Marcelo Fiore and Dmitrij Szamozvancev},
  year = {2022},
  doi = {10.1145/3498715},
  url = {https://doi.org/10.1145/3498715},
  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},
}

@inproceedings{FirsovU13,
  title = {Certified Parsing of Regular Languages},
  author = {Denis Firsov and Tarmo Uustalu},
  year = {2013},
  doi = {10.1007/978-3-319-03545-1_7},
  url = {http://dx.doi.org/10.1007/978-3-319-03545-1_7},
  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 = {Georges Gonthier and Michael Norrish},
  volume = {8307},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-03544-4},
}

@inproceedings{CockxPD14,
  title = {Overlapping and Order-Independent Patterns - Definitional Equality for All},
  author = {Jesper Cockx and Frank Piessens and Dominique Devriese},
  year = {2014},
  doi = {10.1007/978-3-642-54833-8_6},
  url = {http://dx.doi.org/10.1007/978-3-642-54833-8_6},
  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 = {Zhong Shao},
  volume = {8410},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-54832-1},
}

@article{VassenaRGRS19,
  title = {From fine- to coarse-grained dynamic information flow control and back},
  author = {Marco Vassena and Alejandro Russo and Deepak Garg and Vineet Rajani and Deian Stefan},
  year = {2019},
  url = {https://dl.acm.org/citation.cfm?id=3290389},
  researchr = {https://researchr.org/publication/VassenaRGRS19},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
}

@inproceedings{JeffreyP11,
  title = {Integrity Constraints for Linked Data},
  author = {Alan Jeffrey and Peter F. Patel-Schneider},
  year = {2011},
  url = {http://ceur-ws.org/Vol-745/paper_31.pdf},
  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 = {Riccardo Rosati and Sebastian Rudolph and Michael Zakharyaschev},
  volume = {745},
  series = {CEUR Workshop Proceedings},
  publisher = {CEUR-WS.org},
}

@article{AngiuliCMZ21,
  title = {Internalizing representation independence with univalence},
  author = {Carlo Angiuli and Evan Cavallo and Anders Mörtberg and Max Zeuner},
  year = {2021},
  doi = {10.1145/3434293},
  url = {https://doi.org/10.1145/3434293},
  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},
}

@inproceedings{CapriottiKV15,
  title = {Functions out of Higher Truncations},
  author = {Paolo Capriotti and Nicolai Kraus and Andrea Vezzosi},
  year = {2015},
  doi = {10.4230/LIPIcs.CSL.2015.359},
  url = {http://dx.doi.org/10.4230/LIPIcs.CSL.2015.359},
  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 = {Stephan Kreutzer},
  volume = {41},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-939897-90-3},
}

@phdthesis{ethos-1592,
  title = {Agda as a platform for the development of verified railway interlocking systems},
  author = {Karim Kanso},
  year = {2012},
  url = {http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.678306},
  note = {British Library, EThOS},
  researchr = {https://researchr.org/publication/ethos-1592},
  cites = {0},
  citedby = {0},
  school = {Swansea University, UK},
}

@article{AltenkirchC09,
  title = {Big-step normalisation},
  author = {Thorsten Altenkirch and James Chapman and   and  },
  year = {2009},
  doi = {10.1017/S0956796809007278},
  url = {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},
}

@inproceedings{DagandM12,
  title = {Transporting functions across ornaments},
  author = {Pierre-Évariste Dagand and Conor McBride},
  year = {2012},
  doi = {10.1145/2364527.2364544},
  url = {http://doi.acm.org/10.1145/2364527.2364544},
  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 = {Peter Thiemann and Robby Bruce Findler},
  publisher = {ACM},
  isbn = {978-1-4503-1054-3},
}

@inproceedings{Norell09,
  title = {Dependently typed programming in Agda},
  author = {Ulf Norell},
  year = {2009},
  doi = {10.1145/1481861.1481862},
  url = {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 = {Andrew Kennedy and Amal Ahmed},
  publisher = {ACM},
  isbn = {978-1-60558-420-1},
}

@inproceedings{CloustonBGB15,
  title = {Programming and Reasoning with Guarded Recursion for Coinductive Types},
  author = {Ranald Clouston and Ales Bizjak and Hans Bugge Grathwohl and Lars Birkedal},
  year = {2015},
  doi = {10.1007/978-3-662-46678-0_26},
  url = {http://dx.doi.org/10.1007/978-3-662-46678-0_26},
  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 = {Andrew M. Pitts},
  volume = {9034},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-662-46677-3},
}

@inproceedings{Kahl12,
  title = {Towards Certifiable Implementation of Graph Transformation via Relation Categories},
  author = {Wolfram Kahl},
  year = {2012},
  doi = {10.1007/978-3-642-33314-9_6},
  url = {http://dx.doi.org/10.1007/978-3-642-33314-9_6},
  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 = {Wolfram Kahl and Timothy G. Griffin},
  volume = {7560},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-33313-2},
}

@inproceedings{IgriedS16-0,
  title = {Defining Trace Semantics for CSP-Agda},
  author = {Bashar Igried and Anton Setzer},
  year = {2016},
  doi = {10.4230/LIPIcs.TYPES.2016.12},
  url = {https://doi.org/10.4230/LIPIcs.TYPES.2016.12},
  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 = {Silvia Ghilezan and Herman Geuvers and Jelena Ivetic},
  volume = {97},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-95977-065-1},
}

@inproceedings{CicconeDZ21,
  title = {Flexible Coinduction in Agda},
  author = {Luca Ciccone and Francesco Dagnino and Elena Zucca},
  year = {2021},
  doi = {10.4230/LIPIcs.ITP.2021.13},
  url = {https://doi.org/10.4230/LIPIcs.ITP.2021.13},
  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 = {Liron Cohen 0001 and Cezary Kaliszyk},
  volume = {193},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-188-7},
}

@article{Ceulemans2022,
  title = {Sikkel: Multimode Simple Type Theory as an Agda Library},
  author = {Joris Ceulemans and Andreas Nuyts and Dominique Devriese},
  year = {2022},
  month = {jun},
  doi = {10.4204/eptcs.360.5},
  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},
}

@inproceedings{GhaniMF13,
  title = {Positive Inductive-Recursive Definitions},
  author = {Neil Ghani and Lorenzo Malatesta and Fredrik Nordvall Forsberg},
  year = {2013},
  doi = {10.1007/978-3-642-40206-7_3},
  url = {http://dx.doi.org/10.1007/978-3-642-40206-7_3},
  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 = {Reiko Heckel and Stefan Milius},
  volume = {8089},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-40205-0},
}

@article{HuL20,
  title = {Undecidability of $d_{<:}$ and its decidable fragments},
  author = {Jason Z. S. Hu and Ondrej Lhoták},
  year = {2020},
  doi = {10.1145/3371077},
  url = {https://doi.org/10.1145/3371077},
  researchr = {https://researchr.org/publication/HuL20},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {POPL},
}

@inproceedings{Asai19,
  title = {Extracting a call-by-name partial evaluator from a proof of termination},
  author = {Kenichi Asai},
  year = {2019},
  doi = {10.1145/3294032.3294084},
  url = {https://doi.org/10.1145/3294032.3294084},
  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 = {Manuel V. Hermenegildo and Atsushi Igarashi},
  publisher = {ACM},
  isbn = {978-1-4503-6226-9},
}

@inproceedings{McBride10-0,
  title = {Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation},
  author = {Conor McBride},
  year = {2010},
  doi = {10.1145/1863495.1863497},
  url = {http://doi.acm.org/10.1145/1863495.1863497},
  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 = {Bruno C. d. S. Oliveira and Marcin Zalewski},
  publisher = {ACM},
  isbn = {978-1-4503-0251-7},
}

@article{AlgehedB19,
  title = {Simple noninterference from parametricity},
  author = {Maximilian Algehed and Jean-Philippe Bernardy},
  year = {2019},
  doi = {10.1145/3341693},
  url = {https://doi.org/10.1145/3341693},
  researchr = {https://researchr.org/publication/AlgehedB19},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
}

@article{OrtonP18,
  title = {Axioms for Modelling Cubical Type Theory in a Topos},
  author = {Ian Orton and Andrew M. Pitts},
  year = {2018},
  doi = {10.23638/LMCS-14(4:23)2018},
  url = {https://doi.org/10.23638/LMCS-14(4:23)2018},
  researchr = {https://researchr.org/publication/OrtonP18},
  cites = {0},
  citedby = {0},
  journal = {Logical Methods in Computer Science},
  volume = {14},
  number = {4},
}

@inproceedings{VassenaR16,
  title = {On Formalizing Information-Flow Control Libraries},
  author = {Marco Vassena and Alejandro Russo},
  year = {2016},
  doi = {10.1145/2993600.2993608},
  url = {http://doi.acm.org/10.1145/2993600.2993608},
  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 = {Toby C. Murray and Deian Stefan},
  publisher = {ACM},
  isbn = {978-1-4503-4574-3},
}

@article{0001OV18,
  title = {Decidability of conversion for type theory in type theory},
  author = {Andreas Abel and Joakim Öhman and Andrea Vezzosi},
  year = {2018},
  doi = {10.1145/3158111},
  url = {http://doi.acm.org/10.1145/3158111},
  researchr = {https://researchr.org/publication/0001OV18},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {POPL},
}

@article{AllaisA0MM18,
  title = {A type and scope safe universe of syntaxes with binding: their semantics and proofs},
  author = {Guillaume Allais and Robert Atkey and James Chapman and Conor McBride and James McKinna},
  year = {2018},
  doi = {10.1145/3236785},
  url = {https://doi.org/10.1145/3236785},
  researchr = {https://researchr.org/publication/AllaisA0MM18},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {ICFP},
}

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

@inproceedings{CockxME0N22,
  title = {Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs},
  author = {Jesper Cockx and Orestis Melkonian and Lucas Escot and James Chapman and Ulf Norell},
  year = {2022},
  doi = {10.1145/3546189.3549920},
  url = {https://doi.org/10.1145/3546189.3549920},
  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 = {Nadia Polikarpova},
  publisher = {ACM},
  isbn = {978-1-4503-9438-3},
}

@misc{https:-doi.org-10.48550-arxiv.2212.07735,
  title = {Higher-order Games with Dependent Types},
  author = {Escardo, Martin and Oliva, Paulo},
  year = {2022},
  doi = {10.48550/ARXIV.2212.07735},
  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},
}

@inproceedings{Veltri15,
  title = {Two set-based implementations of quotients in type theory},
  author = {Niccolò Veltri},
  year = {2015},
  url = {http://ceur-ws.org/Vol-1525/paper-14.pdf},
  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 = {Jyrki Nummenmaa and Outi Sievi-Korte and Erkki Mäkinen},
  volume = {1525},
  series = {CEUR Workshop Proceedings},
  publisher = {CEUR-WS.org},
}

@inproceedings{AltenkirchK16-0,
  title = {Normalisation by Evaluation for Dependent Types},
  author = {Thorsten Altenkirch and Ambrus Kaposi},
  year = {2016},
  doi = {10.4230/LIPIcs.FSCD.2016.6},
  url = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.6},
  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 = {Delia Kesner and Brigitte Pientka},
  volume = {52},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-95977-010-1},
}

@article{CurtisM15,
  title = {Calculating a linear-time solution to the densest-segment problem},
  author = {Sharon A. Curtis and Shin-Cheng Mu},
  year = {2015},
  doi = {10.1017/S095679681500026X},
  url = {http://dx.doi.org/10.1017/S095679681500026X},
  researchr = {https://researchr.org/publication/CurtisM15},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {25},
}

@inproceedings{VeltriW19,
  title = {Guarded Recursion in Agda via Sized Types},
  author = {Niccolò Veltri and Niels van der Weide},
  year = {2019},
  doi = {10.4230/LIPIcs.FSCD.2019.32},
  url = {https://doi.org/10.4230/LIPIcs.FSCD.2019.32},
  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 = {Herman Geuvers},
  volume = {131},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-95977-107-8},
}

@article{KansoS16,
  title = {A light-weight integration of automated and interactive theorem proving},
  author = {Karim Kanso and Anton Setzer},
  year = {2016},
  doi = {10.1017/S0960129514000140},
  url = {http://dx.doi.org/10.1017/S0960129514000140},
  researchr = {https://researchr.org/publication/KansoS16},
  cites = {0},
  citedby = {0},
  journal = {Mathematical Structures in Computer Science},
  volume = {26},
  number = {1},
  pages = {129-153},
}

@inproceedings{DagandM13,
  title = {A Categorical Treatment of Ornaments},
  author = {Pierre-Évariste Dagand and Conor McBride},
  year = {2013},
  doi = {10.1109/LICS.2013.60},
  url = {http://doi.ieeecomputersociety.org/10.1109/LICS.2013.60},
  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},
}

@inproceedings{AltenkirchLR14,
  title = {Some constructions on ω-groupoids},
  author = {Thorsten Altenkirch and Nuo Li and Ondrej Rypacek},
  year = {2014},
  doi = {10.1145/2631172.2631176},
  url = {http://doi.acm.org/10.1145/2631172.2631176},
  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 = {Amy P. Felty and Brigitte Pientka},
  publisher = {ACM},
  isbn = {978-1-4503-2817-3},
}

@inproceedings{ChapmanUV15,
  title = {Quotienting the Delay Monad by Weak Bisimilarity},
  author = {James Chapman and Tarmo Uustalu and Niccolò Veltri},
  year = {2015},
  doi = {10.1007/978-3-319-25150-9_8},
  url = {http://dx.doi.org/10.1007/978-3-319-25150-9_8},
  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 = {Martin Leucker and Camilo Rueda and Frank D. Valencia},
  volume = {9399},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-25149-3},
}

@inproceedings{DiehlS16,
  title = {Generic lookup and update for infinitary inductive-recursive types},
  author = {Larry Diehl and Tim Sheard},
  year = {2016},
  doi = {10.1145/2976022.2976031},
  url = {http://doi.acm.org/10.1145/2976022.2976031},
  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 = {James Chapman and Wouter Swierstra},
  publisher = {ACM},
  isbn = {978-1-4503-4435-7},
}

@article{NuytsVD17,
  title = {Parametric quantifiers for dependent type theory},
  author = {Andreas Nuyts and Andrea Vezzosi and Dominique Devriese},
  year = {2017},
  doi = {10.1145/3110276},
  url = {http://doi.acm.org/10.1145/3110276},
  researchr = {https://researchr.org/publication/NuytsVD17},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {1},
  number = {ICFP},
}

@article{RestPRVM22,
  title = {Intrinsically-typed definitional interpreters à la carte},
  author = {Cas van der Rest and Casper Bach Poulsen and Arjen Rouvoet and Eelco Visser and Peter D. Mosses},
  year = {2022},
  doi = {10.1145/3563355},
  url = {https://doi.org/10.1145/3563355},
  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},
}

@inproceedings{OlmosFSGGP20,
  title = {A formalisation of LEGv8 in Agda},
  author = {Santiago Arranz Olmos and Martín-Fernández and Matías Steinberg and Alejandro Gadea and Emmanuel Gunther and Miguel Pagano},
  year = {2020},
  doi = {10.1145/3427081.3427086},
  url = {https://doi.org/10.1145/3427081.3427086},
  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 = {Everton Cavalcante and Francisco Dantas and Thaís Batista},
  publisher = {ACM},
  isbn = {978-1-4503-8943-3},
}

@inproceedings{MaarandU18,
  title = {Certified Foata Normalization for Generalized Traces},
  author = {Hendrik Maarand and Tarmo Uustalu},
  year = {2018},
  doi = {10.1007/978-3-319-77935-5_21},
  url = {https://doi.org/10.1007/978-3-319-77935-5_21},
  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 = {Aaron Dutle and César A. Muñoz and Anthony Narkawicz},
  volume = {10811},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-77935-5},
}

@article{SculthorpeH14,
  title = {Work it, wrap it, fix it, fold it},
  author = {Neil Sculthorpe and Graham Hutton},
  year = {2014},
  doi = {10.1017/S0956796814000045},
  url = {http://dx.doi.org/10.1017/S0956796814000045},
  researchr = {https://researchr.org/publication/SculthorpeH14},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {24},
  number = {1},
  pages = {113-127},
}

@phdthesis{hal-3916,
  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 = {Nicolas Pouillard},
  year = {2012},
  url = {https://tel.archives-ouvertes.fr/tel-00759059},
  researchr = {https://researchr.org/publication/hal-3916},
  cites = {0},
  citedby = {0},
  school = {Paris Diderot University, France},
}

@inproceedings{Danielsson12,
  title = {Bag Equivalence via a Proof-Relevant Membership Relation},
  author = {Nils Anders Danielsson},
  year = {2012},
  doi = {10.1007/978-3-642-32347-8_11},
  url = {http://dx.doi.org/10.1007/978-3-642-32347-8_11},
  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 = {Lennart Beringer and Amy P. Felty},
  volume = {7406},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-32346-1},
}

@inproceedings{AllaisMB13,
  title = {New equations for neutral terms: a sound and complete decision procedure, formalized},
  author = {Guillaume Allais and Conor McBride and Pierre Boutillier},
  year = {2013},
  doi = {10.1145/2502409.2502411},
  url = {http://doi.acm.org/10.1145/2502409.2502411},
  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 = {Stephanie Weirich},
  publisher = {ACM},
  isbn = {978-1-4503-2384-0},
}

@inproceedings{ChapmanKNW19,
  title = {System F in Agda, for Fun and Profit},
  author = {James Chapman and Roman Kireev and Chad Nester and Philip Wadler},
  year = {2019},
  doi = {10.1007/978-3-030-33636-3_10},
  url = {https://doi.org/10.1007/978-3-030-33636-3_10},
  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 = {Graham Hutton},
  volume = {11825},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-33636-3},
}

@article{EscotC22,
  title = {Practical generic programming over a universe of native datatypes},
  author = {Lucas Escot and Jesper Cockx},
  year = {2022},
  doi = {10.1145/3547644},
  url = {https://doi.org/10.1145/3547644},
  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},
}

@inproceedings{Allais17,
  title = {Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic},
  author = {Guillaume Allais},
  year = {2017},
  doi = {10.4230/LIPIcs.TYPES.2017.1},
  url = {https://doi.org/10.4230/LIPIcs.TYPES.2017.1},
  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 = {Andreas Abel 0001 and Fredrik Nordvall Forsberg and Ambrus Kaposi},
  volume = {104},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-95977-071-2},
}