PapersUsingAgda

There is also a list of publications using Agda available at https://researchr.org/bibliography/agda-papers/publications, which can be exported to BibTeX and other formats.

List of papers sorted by name of first author:

A

• Copatterns by Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer (POPL 2013).
• Normalization by Evaluation in the Delay Monad by Andreas Abel and James Chapman (MSFP 2014).
• A Formalized Proof of Strong Normalization for Guarded Recursive Types by Andreas Abel and Andrea Vezzosi (APLAS 2014).
• Programming and Reasoning with Infinite Structures Using Copatterns and Sized Types by Andreas Abel (SE 2014).
• Compositional Coinduction with Sized Types by Andreas Abel (CMCS 2016).
• Normalization by evaluation for sized dependent types by Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (ICFP 2017).
• Interactive programming in Agda - Objects and graphical user interfaces by Andreas Abel, Stephan Adelsberger, and Anton Setzer (JFP 2017).
• Decidability of Conversion for Type Theory in Type Theory by Andreas Abel, Joakim Öhman, and Andrea Vezzosi (POPL 2018).
• POPLMark reloaded: Mechanizing proofs by logical relations by Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer and Kathrin Stark (JFP 2019)
• Leibniz equality is isomorphic to Martin-Löf identity, parametrically by Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, and Philip Wadler (JFP 2020).
• Type-preserving compilation via dependently typed syntax by Andreas Abel (TYPES 2020)
• Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda by Andreas Abel (arXiv 2021).
• A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized by Andreas Abel, Nils Anders Danielsson, and Oskar Eriksson (ICFP 2023).
• Regular Expressions in Agda by Alexandre Agular and Bassel Mannaa (Technical Report, 2009)
• When Is a Container a Comonad? by Danel Ahman, James Chapman and Tarmo Uustalu (FoSSaCS 2012).
• When Is a Container a Comonad? by Danel Ahman, James Chapman and Tarmo Uustalu (LMCS 2014).
• Normalization by evaluation and algebraic effects by Danel Ahman and Sam Staton (MFPS 2013).
• Asynchronous effects by Danel Ahman and Matija Pretnar (POPL 2021).
• Non-wellfounded trees in Homotopy Type Theory by Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti (TLCA 2015)
• Reduction monads and their signatures by Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi (POPL 2020).
• Intrinsically Correct Sorting in Cubical Agda by Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide (CPP 2025).
• Mechanised Relation-Algebraic Order Theory in Ordered Categories without Meets by Musa Al-hassy and Wolfram Kahl, RAMICS 2014.
• Simple noninterference from parametricity by Maximilian Algehed and Jean-Philippe Bernardy (ICFP 2019).
• Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control by Fahad Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer (TYPES 2021).
• A model of Solidity-style smart contracts in Agda by Fahad Alhabardi and Anton Setzer (AIBThings 2023).
• A simulator of Solidity-style smart contracts verified in Agda by Fahad Alhabardi and Anton Setzer (ICBTA 2023).
• New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized by Guillaume Allais, Conor McBride and Pierre Boutillier (DTP 2013).
• Certified Proof Search for Intuitionistic Linear Logic by Guillaume Allais, Conor McBride
• Typing with Leftovers - A Mechanization of Intuitionistic Linear Logic by Guillaume Allais (TYPES 2017 post-proceedings).
• Type-and-Scope Safe Programs and Their Proofs by Guillaume Allais, James Chapman, Conor McBride, James McKinna (CPP 2017)
• A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs by Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna (ICFP 2018)
• Generic Level Polymorphic N-ary Functions by Allais Guillaume (TYDE 2019)
• Big-Step Normalisation by Thorsten Altenkirch and James Chapman (JFP 2009).
• Monads need not be endofunctors by Thorsten Altenkirch, James Chapman and Tarmo Uustalu (FoSSaCS 2010).
• Monads need not be endofunctors by Thorsten Altenkirch, James Chapman and Tarmo Uustalu (LMCS 2015).
• Relative monads formalised by Thorsten Altenkirch, James Chapman and Tarmo Uustalu (JFR 2014).
• Termination Checking in the Presence of Nested Inductive and Coinductive Types by Thorsten Altenkirch and Nils Anders Danielsson.
• Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type by Thorsten Altenkirch, Nils Anders Danielsson and Nicolai Kraus (FoSSaCS 2017).
• Type Theory in Type Theory using Quotient Inductive Types by Thorsten Altenkirch and Ambrus Kaposi (POPL 2016).
• Normalisation by Evaluation for Dependent Types by Thorsten Altenkirch and Ambrus Kaposi (FSCD 2016).
• Some constructions on ω-groupoids by Thorsten Altenkirch, Nuo Li and Ondřej Rypáček (LFMTP 2014).
• Observational Equality, Now! by Thorsten Altenkirch, Conor McBride and Wouter Swierstra (PLPV 2007).
• Indexed Containers by Thorsten Altenkirch and Peter Morris (LICS 2009).
• Indexed Containers by Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride and Peter Morris (JFP).
• A Syntactical Approach to Weak ω-Groupoids by Thorsten Altenkirch and Ondřej Rypáček (CSL 2012; with accompanying Agda formalisation).
• Homotopical Patch Theory (Expanded Version) by Carlo Angiuli, Edward Morehouse, Daniel R. Licata and Robert Harper (ICFP 2014; some proofs formalised using Agda).
• Internalizing representation independence with univalence by Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner (POPL 2021).
• Extracting a Call-by-Name Partial Evaluator from a Proof of Termination by Kenichi Asai (PEPM 2019, formalisation)
• A Type Theoretic Specification of Partial Evaluation by Kenichi Asai, Luminous Fennell, Peter Thiemann and Yang Zhang (PPDP 2014)
• Refining Inductive Types by Robert Atkey, Patricia Johann and Neil Ghani (LMCS 2012).
• When is a Type Refinement an Inductive Type? by Robert Atkey, Patricia Johann and Neil Ghani (FOSSACS 2011).
• A Semantic Proof of Generalised Cut Elimination for Deep Inference by Robert Atkey and Wen Kokke (MFPS 2024)

B

• Intrinsically-typed definitional interpreters for imperative languages by Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser, PACMPL 2(POPL): 16:1-16:34 (2018).
• Formalisation of Dependent Type Theory: The Example of CaTT by Thibaut Benjamin (TYPES 2021).
• Proofs for Free -- Parametricity for Dependent Types by J-P Bernardy, P Jansson, R Paterson (JFP 2012) - an extended version of (ICFP 2010).
• Parametricity and dependent types by Jean-Philippe Bernardy, Patrik Jansson and Ross Paterson (ICFP 2010). Superseded by the extended version "Proofs for Free" (JFP 2012).
• Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda. by Jean-Philippe Bernardy and Patrik Jansson, 2016.
• Importing Agda Proofs in Logipedia by Frédéric Blanqui and Guillaume Genestier (MSc internship, 2019)
• Another Look at Function Domains by Ana Bove (MFPS 2009).
• Dependent Types at Work by Ana Bove and Peter Dybjer (LerNet ALFA Summer School 2008).
• A Brief Overview of Agda - A Functional Language with Dependent Types by Ana Bove, Peter Dybjer and Ulf Norell (TPHOLs 2009).
• Combining interactive and automatic reasoning in first order theories of functional programs by Ana Bove, Peter Dybjer, and Andrés Sicard-Ramírez (FoSSaCS 2012).
• Embedding a logical theory of constructions in Agda by Ana Bove, Peter Dybjer, and Andrés Sicard-Ramírez (PLPV 2009).
• Synthetic Integral Cohomology in Cubical Agda by Guillaume Brunerie, Axel Ljungström, Anders Mörtberg (CSL 2022).

C

• A theory of changes for higher-order languages — incrementalizing λ-calculi by static differentiation by Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, and Klaus Ostermann (PLDI 2014; formalised)
• Formalizing Constructive Projective Geometry in Agda by Guillermo Calderón (LSFA 2017; Agda Formalization)
• Static Balance Checking for First-Class Modular Systems of Equations by John Capper and Henrik Nilsson (TFP 2010; formalised using Agda).
• Towards a Formal Semantics for a Structurally Dynamic Noncausal Modelling Language by John Capper and Henrik Nilsson (TLDI 2012).
• Functions out of Higher Truncations by Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi, CSL 2015.
• Computing with Semirings and Weak Rig Groupoids by Jacques Carette and Amr Sabry (ESOP 2016).
• Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study by Jacques Carette, William M. Farmer
• Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda by Harold Carr, Christa Jenkins, Mark Moir, Victor Cacciari Miraldo, Lisandra Silva (NFM 2022).
• Sikkel: Multimode Simple Type Theory as an Agda Library by Joris Ceulemans, Andreas Nuyts, Dominique Devriese (MSFP 2022).
• BiSikkel: A Multimode Logical Framework in Agda by Joris Ceulemans, Andreas Nuyts, Dominique Devriese (POPL 2025).
• Dijkstra’s Algorithm without the distributivity axiom: a proof of correctness in Agda by Leonhard D. Markert and Dominic P. Mulligan, 2016.
• The Extended UTXO Model by Manuel M.T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Michael Peyton Jones, and Philip Wadler (WTSC @ FC 2020).
• UTXOma: UTXO with Multi-Asset Support by Manuel M.T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones, Polina Vinogradova, Philip Wadler, and Joachim Zahnentferner (ISoLA 2020).
• Native Custom Tokens in the Extended UTXO Model by Manuel M.T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones, Polina Vinogradova, and Philip Wadler (ISoLA 2020).
• Type Theory should eat itself by James Chapman (LFMTP 2008).
• The Gentle Art of Levitation by James Chapman, Pierre-Évariste Dagand, Conor McBride and Peter Morris (ICFP 2010; formalised using Agda).
• Formalizing restriction categories by James Chapman, Tarmo Uustalu, Niccolň Veltri (JFR 2017).
• Quotienting the delay monad by weak bisimilarity by James Chapman, Tarmo Uustalu, Niccolň Veltri (ICTAC 2015).
• Quotienting the delay monad by weak bisimilarity by James Chapman, Tarmo Uustalu, Niccolň Veltri (MSCS 2019).
• System F in Agda, for Fun and Profit by James Chapman, Roman Kireev, Chad Nester, Philip Wadler (MPC 2019).
• Fractional Types: Expressive and Safe Space Management for Ancilla Bits by Chao-Hong Chen, Vikraman Choudhury, Jacques Carette, Amr Sabry
• A computational interpretation of compact closed categories: reversible programming with negative and fractional types by Chao-Hong Chen and Amr Sabry (POPL 2021).
• Functional Pearl: Folding Polynomials of Polynomials by Chen-Mou Cheng, Ruey-Lin Hsu, and Shin-Cheng Mu (FLOPS 2018).
• Monadic typed tactic programming by reflection by Liang-Ting Chen (TYDE 2019)
• Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda by Liang-Ting Chen, Fredrik Nordvall Forsberg, Tzu-Chun Tsai (CPP 2026).
• Formal derivation of greedy algorithms from relational specifications: A tutorial by Yu-Hsi Chiang and Shin-Cheng Mu (JLAMP, in press).
• Flexible Coinduction in Agda by Luca Ciccone (MSc thesis)
• A Dependently Typed Linear π-Calculus in Agda by Luca Ciccone and Luca Padovani (PPDP 2020).
• Flexible Coinduction in Agda by Luca Ciccone, Francesco Dagnino, and Elena Zucca (ITP 2021).
• Programming and Reasoning with Guarded Recursion for Coinductive Types by Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl and Lars Birkedal (FOSSACS 2015; Agda implementation).
• Overlapping and order-independent patterns: Definitional equality for all by Jesper Cockx, Dominique Devriese, and Frank Piessens (ESOP 2014).
• Pattern matching without K by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2014).
• Sprinkles of extensionality for your vanilla type theory by Jesper Cockx and Andreas Abel (TYPES 2016), extended abstract.
• Unifiers as equivalences: Proof-relevant unification of dependently typed data by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2016).
• Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules by Jesper Cockx (TYPES 2019).
• The taming of the rew: A type theory with computational assumptions by Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter (POPL 2021).
• Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs by Jesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman, and Ulf Norell (Haskell @ ICFP 2022).
• Principal Type Scheme for Session Types by Ernesto Copello, Nora Szasz and Álvaro Tasistro (International Journal of Logic and Computation; accompanying Agda code).
• Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda by Ernesto Copello, Álvaro Tasistro and Bruno Bianchi (SBLP 2014).
• Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders by Ernesto Copello, Nora Szasz, Álvaro Tasistro (LFMTP@FSCD 2018: 11-26).
• Isomorphism Is Equality by Thierry Coquand and Nils Anders Danielsson (Indagationes Mathematicae).
• Calculating a linear-time solution to the densest-segment problem by Sharon Curtis and Shin-Cheng Mu (JFP 2015; Agda formalisation).

D

• The Essence of Ornaments by Pierre-Evariste Dagand (Agda model).
• A Categorical Treatment of Ornaments by Pierre-Evariste Dagand and Conor McBride (LICS 2013; Agda model).
• Transporting Functions across Ornaments by Pierre-Evariste Dagand and Conor McBride (ICFP 2012; Agda model).
• Transporting Functions across Ornaments by Pierre-Évariste Dagand and Conor McBride (JFP; Agda model).
• A Relaxation of Üresin and Dubois’ Asynchronous Fixed-Point Theory in Agda by Matthew Daggit, Ran Zmigrod and Timothy G. Griffin (JAR 2019)
• The Agda standard library: version 2.0 by Matthew L. Daggitt, Guillaume Allais, James McKinna, Andreas Abel, et al. (JOSS 2025).
• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family by Nils Anders Danielsson (TYPES 2006). (Uses AgdaLight, a close relative of Agda.)
• A Formalisation of the Correctness Result From "Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures" by Nils Anders Danielsson.
• Bag Equivalence via a Proof-Relevant Membership Relation by Nils Anders Danielsson (ITP 2012).
• Beating the Productivity Checker Using Embedded Languages by Nils Anders Danielsson (PAR 2010).
• Correct-by-Construction Pretty-Printing by Nils Anders Danielsson (DTP 2013).
• Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures by Nils Anders Danielsson (POPL 2008).
• Operational Semantics Using the Partiality Monad by Nils Anders Danielsson (ICFP 2012).
• Total Parser Combinators by Nils Anders Danielsson (ICFP 2010).
• Mixing Induction and Coinduction by Nils Anders Danielsson and Thorsten Altenkirch.
• Subtyping, Declaratively: An Exercise in Mixed Induction and Coinduction by Nils Anders Danielsson and Thorsten Altenkirch (MPC 2010).
• Parsing Mixfix Operators by Nils Anders Danielsson and Ulf Norell (IFL 2008).
• Mechanically Verified Calculational Abstract Interpretation by David Darais and David Van Horn.
• Constructive Galois Connections: Tracking Soundness without Formulas by David Darais and David Van Horn (JFP 2019).
• A Machine-Checked Proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory by William DeMeo and Jacques Carette (TYPES 2021).
• On the Bright Side of Type Classes: Instance Arguments in Agda by Dominique Devriese and Frank Piessens (ICFP 2011).
• Typed Syntactic Metaprogramming by Dominique Devriese and Frank Piessens (ICFP 2013).
• Verified Stack-Based Genetic Programming via Dependent Types by Larry Diehl (AAIP 2011).
• Leveling Up Dependent Types: Generic programming over a predicative hierarchy of universes. By Larry Diehl and Tim Sheard (DTP 2013).
• Generic Constructors and Eliminators from Descriptions: Type Theory as a Dependently Typed Internal DSL By Larry Diehl and Tim Sheard (WGP 2014).
• Generic Lookup and Update for Infinitary Inductive-Recursive Types by Larry Diehl and Tim Sheard
• Computing with generic trees in Agda by Stephen Dolan (TyDe 2022).
• Automating Boundary Filling in Cubical Agda by Maximilian Doré, Evan Cavallo, Anders Mörtberg (FSCD 2024).

E

• Multiple Conclusion Linear Logic: Cut-elimination and more. by Harley Eades III and Valeria de Paiva (LFCS 2016).
• Dualized Simple Type Theory by Harley Eades III, Aaron Stump, and Ryan McCleeary (LMCS 2016)
• Proposing a New Foundation of Attack Trees in Monoidal Categories by Harley Eades III
• Timely Computation by Conal Elliott (ICFP 2023).
• An Agda formalization of modalities and erasures in a dependently typed language by Oskar Eriksson (MSc thesis, Chalmers University, 2021).
• Graded Modal Type Theory, Formalized by Oskar Eriksson (Licentiate thesis, University of Gothenburg, 2025).
• Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics by Martin Escardó (JSL 2013, vol. 78(3)).
• Continuity of Gödel's system T functionals via effectful forcing by Martin Escardó, MFPS'2013. ENTCS 01/2013;298:119–141.
• The intrinsic topology of a Martin-Löf universe by Martin Escardó, 4WFT (Fourth Workshop on Formal Topology), Ljubljana, Slovenia, June 2012 (Agda code).
• Searchable Sets, Dubuc-Penon Compactness, Omniscience Principles, and the Drinker Paradox by Martı́n Escardó and Paulo Oliva (in CiE 2010 booklet; Agda code).
• What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common by Martin Escardó and Paulo Oliva (MSFP 2010).
• The intrinsic topology of Martin-Löf universes by Martı́n Hötzel Escardó and Thomas Streicher (accepted for publication in Annals of Pure and Applied Logic; referenced Agda code).
• A constructive manifestation of the Kleene-Kreisel continuous functionals by Martı́n Escardó and Chuangjie Xu (accepted for publication in Annals of Pure and Applied Logic; Agda code).
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation by Martin Escardó and Chuangjie Xu, TLCA'2015.
• Practical generic programming over a universe of native datatypes by Lucas Escot, Jesper Cockx (ICFP 2022).

F

• Validity, Liquidity, and Fidelity: Formal Verification for Smart Contracts in Cardano by Tudor Ferariu, Philip Wadler, and Orestis Melkonian (FMBC @ ETAPS 2025).
• Translating Proofs from Impredicative to Predicative Systems by Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal (CSL 2023).
• Formal metatheory of second-order abstract syntax by Marcelo Fiore and Dmitrij Szamozvancev (POPL 2022).
• Certified parsing of regular languages by Denis Firsov and Tarmo Uustalu (CPP 2013).
• Certified CYK parsing of context-free languages by Denis Firsov and Tarmo Uustalu (JLAMP 2014).
• Certified normalization of context-free grammars by Denis Firsov and Tarmo Uustalu (CPP 2015).
• Dependently typed programming with finite sets by Denis Firsov and Tarmo Uustalu (WGP 2015).
• Variations on Noetherianness by Denis Firsov, Tarmo Uustalu and Niccolň Veltri (MSFP 2016).
• A Calculus for Esterel: If can, can. If no can, no can by Spencer P. Florence, Shu-Hung You, Jesse A. Tov, and Robby Findler (POPL 2019).
• Inductive-inductive Definitions by Fredrik Nordvall Forsberg and Anton Setzer (CSL 2010; Agda formalisation).
• Integrating an Automated Theorem Prover into Agda by Simon Foster and Georg Struth (3rd NASA Formal Methods Symposium).
• Distributed call-by-value machines by Olle Fredriksson.
• Krivine Nets: A semantic foundation for distributed execution by Olle Fredriksson and Dan R. Ghica (ICFP 2014).

G

• Nominal techniques as an Agda library by Murdoch J. Gabbay and Orestis Melkonian (TYPES 2023), extended abstract.
• Specification and Verification of a Linear-Time Temporal Logic for Graph Transformation by Fabio Gadducci, Alessandro Laretto, and Davide Trotta (CALCO/GG 2023).
• Encoding Agda Programs Using Rewriting by Guillaume Genestier (FSCD 2020).
• An Algebraic Foundation and Implementation of Induction Recursion and Indexed Induction Recursion by Neil Ghani and Peter Hancock.
• Positive Inductive-Recursive Definitions by Neil Ghani, Lorenzo Malatesta and Fredrik Nordvall Forsberg (LMCS; Agda development).
• Fibred Data Types by Neil Ghani, Lorenzo Malatesta, Fredrik Nordvall Forsberg and Anton Setzer (LICS 2013).
• Definitional Proof-Irrelevance without K by Gaetan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau (POPL 2019).
• Staged Multi-Result Supercompilation: Filtering by Transformation. by Sergei Grechanik, Ilya Klyuchnikov and Sergei Romanenko (Meta 2014; slides, Agda source).
• Asynchronous Convergence of Policy-Rich Distributed Bellman-Ford Routing Protocols by Griffin, T. G., Daggitt, M., & Gurney, A. (ACM SIGCOMM 2018)
• Löb's theorem: A functional pearl of dependently typed quining by Jason Gross, Jack Gallagher and Benya Fallenstein.

H

• Initial Algebra Semantics for Cyclic Sharing Tree Structures by Makoto Hamana (LMCS 2010).
• A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach by Makoto Hamana and Marcelo Fiore (WGP 2011).
• Programming interfaces and basic topology by Peter Hancock and Pierre Hyvernat (Annals of Pure and Applied Logic; accompanying Agda code).
• Small Induction Recursion by Peter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta and Thorsten Altenkirch (TLCA 2013).
• Higher-Dimensional Types in the Mechanization of Homotopy Theory by Kuen-Bang Hou (Favonia), PhD thesis.
• A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory by Kuen-Bang Hou (Favonia), Eric Finster, Danial R. Licata and Peter LeFanu Lumsdaine (LICS 2016).
• The Seifert–van Kampen Theorem in Homotopy Type Theory by Kuen-Bang Hou (Favonia) and Michael Shulman (CSL 2016).
• Formalizing category theory in Agda by Jason Z. S. Hu and Jacques Carette (CPP 2021).
• Undecidability of D<: and Its Decidable Fragments by Jason Z. S. Hu and Ondřej Lhoták (POPL 2020).
• Compiling Concurrency Correctly: Cutting Out the Middle Man by Liyang HU and Graham Hutton (TFP 2009).

I

• Dependently-typed programming in scientific computing: Examples from economic modelling by Cezar Ionescu and Patrik Jansson (IFL 2012).
• Testing versus proving in climate impact research by Cezar Ionescu and Patrik Jansson (TYPES2011).

J

• How to do proofs: practically proving properties about effectful programs' results (functional pearl) by Koen Jacobs, Andreas Nuyts, Dominique Devriese (TYDE 2019)
• A readable and computable formalization of the Streamlet consensus protocol by Mauro Jaskelioff, Orestis Melkonian, and James Chapman (FMBC @ ETAPS 2025).
• The Lax Braided Structure of Streaming I/O by Alan Jeffrey and Julian Rathke (CSL 2011).
• Integrity Constraints for Linked Data by Alan Jeffrey and Peter F. Patel Schneider (DL 2011).
• LTL Types FRP by Alan Jeffrey (PLPV 2012).
• Causality For Free!: Parametricity Implies Causality for Functional Reactive Programs by Alan Jeffrey (PLPV 2013).
• Dependently Typed Web Client Applications: FRP in Agda in HTML5 by Alan Jeffrey (PADL 2013).
• Functional Reactive Types by Alan Jeffrey (CSL-LICS 2014; Agda source).
• Constructive Final Semantics of Finite Bags by Philipp Joram, Niccolň Veltri (ITP 2023).
• Pinpointing the Learning Obstacles of an Interactive Theorem Prover by Sára Juhošová, Andy Zaidman, and Jesper Cockx (ICPC 2025).

K

• Dependently-Typed Formalisation of Typed Term Graphs by Wolfram Kahl, TERMGRAPH 2011.
• Dependently-Typed Formalisation of Relation-Algebraic Abstractions by Wolfram Kahl, RAMICS 2011.
• Towards Certifiable Implementation of Graph Transformation via Relation Categories by Wolfram Kahl, RAMICS 2012.
• A Mechanised Abstract Formalisation of Concept Lattices by Wolfram Kahl, RAMICS 2014.
• A Light-Weight Integration of Automated and Interactive Theorem Proving by Karim Kanso and Anton Setzer.
• Constructing quotient inductive-inductive types by Ambrus Kaposi, András Kovács, and Thorsten Altenkirch (POPL 2019).
• Hereditary Substitutions for Simple Types, Formalized by Chantal Keller and Thorsten Altenkirch (MSFP 2010).
• Algebras for weighted search by Donnacha Oisín Kidney and Nicolas Wu (ICFP 2021).
• Algebraic Effects Meet Hoare Logic in Cubical Agda by Donnacha Oisín Kidney, Zhixuan Yang, Nicolas Wu (POPL 2024).
• On the Agda Language (in Japanese) by Yoshiki Kinoshita.
• Category Theoretic Structure of Setoids by Yoshiki Kinoshita and John Power (TCS).
• Human and machine-readable models of state machines for the Cardano ledger by Andre Knispel, James Chapman, Orestis Melkonian, and Polina Vinogradova (FMBC @ CAV 2022), extended abstract.
• Formal specification of the Cardano blockchain ledger, mechanized in Agda by Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell (FMBC @ ETAPS 2024).
• Modularising Inductive Families by Hsiang-Shang Ko and Jeremy Gibbons (Progress in Informatics 2013).
• Modularising Inductive Families by Hsiang-Shang Ko and Jeremy Gibbons (WGP 2011).
• Relational algebraic ornaments by Hsiang-Shang Ko and Jeremy Gibbons (DTP 2013).
• Programming metamorphic algorithms in Agda (functional pearl) by Hsiang-Shang Ko
• Datatype-generic programming meets elaborator reflection by Hsiang-Shang Ko, Liang-Ting Chen, and Tzu-Di Lin (ICFP 2022).
• Learning Structure-Aware Representations of Dependent Types by Konstantinos Kogkalidis, Orestis Melkonian, and Jean-Philippe Bernardy (NeurIPS 2024).
• Formalising type-logical grammars in Agda by Wen Kokke (TYTLES 2015).
• Auto in Agda: programming proof search using reflection by Wen Kokke and Wouter Swierstra (MPC 2015).
• Programming language foundations in Agda by Wen Kokke, Jeremy G. Siek, and Philip Wadler (SCP 2020).
• Intrinsic Verification of a Regular Expression Matcher by Joomy Korkut, Maksim Trifunovski and Daniel R. Licata.
• Elaboration with first-class implicit function types by András Kovács (ICFP 2020).
• Generalized Universe Hierarchies and First-Class Universe Levels by András Kovács (CSL 2022).
• Generalizations of Hedberg's Theorem by Nicolai Kraus, Martín Escardó, Thierry Coquand and Thorsten Altenkirch (TLCA 2013; formalised in Agda).
• Higher Homotopies in a Hierarchy of Univalent Universes by Nicolai Kraus and Christian Sattler (ACM Transactions on Computational Logic; Agda formalisation).
• Notions of anonymous existence in Martin-Loef Type Theory by Nicolai Kraus, M.H. Escardo, T. Coquand, T. Altenkirch, submitted to LMCS.
• Truncation Levels in Homotopy Type Theory by Nicolai Kraus, PhD thesis.
• Constructions with Non-Recursive Higher Inductive Types by Nicolai Kraus, LICS 2016.
• Agda as a Platform for the Development of Verified Railway Interlocking Systems. by Karim Kanso, PhD thesis.

L

• Plausible sealing for gradual parametricity by Daniel Labrada, Matías Toro, Éric Tanter, and Dominique Devriese (OOPSLA 2022).
• Computing Cohomology Rings in Cubical Agda by Thomas Lamiaux, Axel Ljungström, Anders Mörtberg (CPP 2023).
• Type-safe diff for families of datatypes by Eelco Lempsink, Sean Leather, Andres Löh (WGP 2009).
• A Cubical Approach to Synthetic Homotopy Theory by Daniel R. Licata and Guillaume Brunerie (LICS 2015).
• πn(Sn) in Homotopy Type Theory by Daniel R. Licata and Guillaume Brunerie (invited paper, CPP 2013; proof formalised using Agda).
• Eilenberg-MacLane Spaces in Homotopy Type Theory by Dan Licata and Eric Finster (LICS 2014; with accompanying Agda formalisation).
• A Monadic Formalization of ML5 by Daniel R. Licata and Robert Harper (LFMTP 2010).
• A Universe of Binding and Computation by Daniel R. Licata and Robert Harper (ICFP 2009).
• Positively Dependent Types by Daniel R. Licata and Robert Harper (PLPV 2009).
• Adjoint Logic with a 2-Category of Modes by Daniel R. Licata and Michael Shulman (LFCS 2016; references Agda proofs).
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory by Daniel R. Licata and Michael Shulman (LICS 2013).
• Focusing on Binding and Computation by Daniel R. Licata, Noam Zeilberger, and Robert Harper (LICS 2008).
• Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language by Bohdan Liesnikov and Jesper Cockx (APLAS 2024).
• Formalizing π₄(Sł) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda by Axel Ljungström, Anders Mörtberg (LICS 2023).
• Generic Programming with Indexed Functors by Andres Löh and José Pedro Magalhăes (WGP 2011).

M

• Certified Foata normalization for generalized traces by Hendrik Maarand and Tarmo Uustalu (NFM 2018).
• Certified normalization of generalized traces by Hendrik Maarand and Tarmo Uustalu (ISSE 2019).
• Agda Formalization of a Security-preserving Translation from MiniAgda to ICC* by Camilo Manzino and Alberto Pardo (LSFA 2020).
• Formal Investigation of the Extended UTxO Model by Orestis Melkonian, Wouter Swierstra, and Manuel M.T. Chakravarty (TyDe @ ICFP 2019), extended abstract.
• Program logics for ledgers by Orestis Melkonian, Wouter Swierstra, and James Chapman (TYPES 2023), extended abstract.
• Verified compilation from BitML to Bitcoin: An Agda Odyssey by Orestis Melkonian, PhD thesis, 2024.
• Mechanizing BFT consensus protocols in Agda by Orestis Melkonian, Mauro Jaskelioff, James Chapman, and Jon Rossie (TYPES 2024), extended abstract.
• Program logics for ledgers by Orestis Melkonian, Wouter Swierstra, and James Chapman (FMBC @ ETAPS 2025).
• Mechanized safety of Jolteon consensus in Agda by Orestis Melkonian, Mauro Jaskelioff, and James Chapman (TYPES 2025).
• A Polynomial Testing Principle by Conor McBride.
• Agda-curious? An Exploration of Programming with Dependent Types by Conor McBride (invited talk, ICFP 2012).
• Datatypes of Datatypes by Conor McBride (lecture notes).
• Djinn, Monotonic (extended abstract) by Conor McBride.
• How to Keep Your Neighbours in Order by Conor McBride (ICFP 2014).
• Ornamental Algebras, Algebraic Ornaments by Conor McBride.
• Outrageous but Meaningful Coincidences: Dependent type-safe syntax and evaluation by Conor McBride (WGP 2010).
• Turing-Completeness Totally Free by Conor McBride (MPC 2015).
• Experience in an Adequate Programming of Algebra in a Language with Dependent Types by Sergei D. Meshveliani (PCA '2014).
• O зависимых типах и интуиционизме в программировании математики (On dependent types and intuitionism in programming mathematics) by С. Д. Мешвелиани (S.D. Meshveliani; in Программные системы: Теория и приложения).
• On provable programs for list processing by Sergei D. Meshveliani (PCA '2015).
• Программирование основ вычислительной алгебры на языке с зависимыми типами (Programming basic computer algebra in a language with dependent types) by С. Д. Мешвелиани (Sergei Meshveliani; in Программные системы: Теория и приложения).
• Provable programming of algebra: particular points, examples. by Sergei D. Meshveliani (PCA '2016).
• Introspective Kripke models and normalisation by evaluation for the λ□-calculus by Miëtek Bak
• Formal verification of authenticated, append-only skip lists in Agda by Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, and Guy L. Steele Jr. (CPP 2021).
• Clock Constraints Specification Langage : A mechanized denotational semantics in Agda by Mathieu Montin, Marc Pantel.
• LibNDT: Towards a Formal Library on Spreadable Properties by Mathieu Montin, Virgile Ledein, and Catherine Dubois (MSFP 2022).
• Security-Typed Programming within Dependently-Typed Programming by Jamie Morgenstern and Daniel R. Licata (ICFP 2010).
• Cubical synthetic homotopy theory by Anders Mörtberg, Loďc Pujet (CPP 2020).
• Algebra of programming in Agda: dependent types for relational program derivation by Shin-Cheng Mu, Hsiang-Shang Ko & Patrik Jansson (JFP 2009).
• Algebra of Programming Using Dependent Types by Shin-Cheng Mu, Hsiang-Shang Ko & Patrik Jansson (MPC 2008).

N

• Theorem-proving Verification for Asynchronous Circuits by Shunji Nishimura, Motoki Amagasaki, Morihiro Kuga, Masahiro Iida, Toshinori Sueyoshi (International Journal of Innovative Computing, Information and Control).
• A cost-aware logical framework by Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper (POPL 2022).
• Embedding Polymorphic Dynamic Typing by Thomas van Noort, Wouter Swierstra, Peter Achten, Rinus Plasmeijer (WGP 2011).
• Three Equivalent Ordinal Notation Systems in Cubical Agda by Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani (CPP 2020)
• Dependently Typed Programming in Agda by Ulf Norell (AFP 2008).
• Interactive Programming with Dependent Types by Ulf Norell (invited talk, ICFP 2013; Agda code from talk).
• Parametric Quantifiers for Dependent Type Theory by Andreas Nuyts, Andrea Vezzosi, Dominique Devriese (ICFP 2017).

O

• Applications of applicative proof search by Liam O'Connor (TYDE 2016)
• Deferring the details and deriving programs by Liam O'Connor (TYDE 2019); Agda formalization
• A formalisation of LEGv8 in Agda by Manuel Olmos, Emmanuel Martín-Fernández, Nicolás Steinberg, Alejandro Gadea, Emanuel Gunther, and Miguel Pagano (SBLP 2020).
• Hazelnut: A Bidirectionally Typed Structure Editor Calculus (paper draft) by Cyrus Omar, Michael Hilton, Ian Voysey, Jonathan Aldrich, and Matthew A. Hammer (TFP 2016; Agda formalisation).
• Live Functional Programming with Typed Holes by Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer, POPL 2019.
• Using session types as an effect system by Dominic Orchard and Nobuko Yoshida (PLACES 2015; Agda formalisation).
• Axioms for Univalence by I. Orton and A. M. Pitts, TYPES 2017.
• Axioms for Modelling Cubical Type Theory in a Topos by I. Orton and A. M. Pitts, CSL 2016.
• The Power Of Pi by Nicolas Oury and Wouter Swierstra (ICFP 2008).

P

• Calculating dependently-typed compilers by Mitchell Pickard and Graham Hutton (ICFP 2021).
• A unified treatment of syntax with binders by Nicolas Pouillard and François Pottier (JFP 2012)
• Namely, Painless: A unifying approach to safe programming with first-order syntax with binders by Nicolas Pouillard, PhD thesis
• Nameless, Painless by Nicolas Pouillard (ICFP 2011).
• A fresh look at programming with names and binders by Nicolas Pouillard and François Pottier (ICFP 2010).
• On homotopy of walks and spherical maps in Homotopy Type Theory by Jonathan Prieto-Cubides (CPP 2022).
• Deeper Shallow Embeddings by Anna Schmitt, G. A. Kavvos, and Leonidas Lampropoulos (ITP 2022).
• Observational equality: now for good by Loďc Pujet and Nicolas Tabareau (POPL 2022).
• Impredicative Observational Equality by Loďc Pujet and Nicolas Tabareau (POPL 2023).

Q

R

• Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages by Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser (CPP 2020)
• Intrinsically typed compilation with nameless labels by Arjen Rouvoet, Robbert Krebbers, and Eelco Visser (POPL 2021).

S

• Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer Lemma by Hannes Saffrich, Peter Thiemann, and Marius Weidner (TyDe 2024).
• Modular Type-Safety Proofs in Agda by Christopher Schwaab and Jeremy G. Siek (PLPV 2013).
• Work It, Wrap It, Fix It, Fold It by Neil Sculthorpe and Graham Hutton (formalised using Agda).
• Safe Functional Reactive Programming through Dependent Types by Neil Sculthorpe and Henrik Nilsson (ICFP 2009).
• Generic programming of all kinds by Alejandro Serrano, Victor Cacciari Miraldo (Haskell 2018)
• Gradual Guarantee via Step-Indexed Logical Relations in Agda by Jeremy G. Siek (EPTCS 2024).
• Constructive Provability Logic by Robert J. Simmons and Bernardo Toninho (presented at IMLA 2011).
• Extracting the power of dependent types by Artjoms Sinkarovs and Jesper Cockx (GPCE 2021).
• Correctness Meets Performance: From Agda to Futhark by Artjoms Sinkarovs, Troels Henriksen (ICFP 2025).
• Forward build systems, formally by Sarah Spall, Neil Mitchell, and Sam Tobin-Hochstadt (CPP 2022).
• A theory of higher-order subtyping with type intervals by Sandro Stucki and Paolo G. Giarrusso (ICFP 2021).
• From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine by Wouter Swierstra (MSFP 2012).
• More Dependent Types for Distributed Arrays by Wouter Swierstra (HOSC 2010).
• Sorted: Verifying the Problem of the Dutch National Flag in Type Theory by Wouter Swierstra (JFP 2011).
• Dependent types for Distributed Arrays by Wouter Swierstra and Thorsten Altenkirch (TFP 2008).
• A library for polymorphic dynamic typing by Wouter Swierstra and Thomas van Noort.
• A predicate transformer semantics for effects by Wouter Swierstra and Tim Baanen (ICFP 2019).
• FLABloM: Functional linear algebra with block matrices by Adam Sandberg Eriksson and Patrik Jansson (TYPES 2016), extended abstract.

T

• Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda Calculus by Álvaro Tasistro, Ernesto Copello and Nora Szasz (LSFA 2014).
• Agda Meets Accelerate by Peter Thiemann and Manuel M. T. Chakravarty (IFL 2012).
• Modal μ-Calculus for Free in Agda by Martin Lukáš Todorov, Casper Bach Poulsen (TyDe 2024).
• From algebra to abstract machine: a verified generic construction by Carlos Tomé Cortińas and Wouter Swierstra (TyDe 2018).

U

• Strong Normalization for the Simply-Typed Lambda Calculus in Agda by Ernesto Urciuoli, Álvaro Tasistro, and Nora Szasz (LSFA 2020).
• Coherence for skew-monoidal categories by Tarmo Uustalu (MSFP 2014).
• Finiteness and rational sequences, constructively by Tarmo Uustalu and Niccolň Veltri (JFP 2017).
• Partiality and container monads by Tarmo Uustalu and Niccolň Veltri (APLAS 2017).
• The delay monad and restriction categories by Tarmo Uustalu and Niccolň Veltri (ICTAC 2017).
• The sequent calculus of skew monoidal categories by Tarmo Uustalu, Niccolň Veltri and Noam Zeilberger (MFPS XXXIV).
• Proof theory of partially normal skew monoidal categories by Tarmo Uustalu, Niccolň Veltri and Noam Zeilberger (ACT 2020)

V

• Normalization for Fitch-style modal calculi by Nachiappan Valliappan, Fabian Ruch, and Carlos Tomé Cortińas (ICFP 2022).
• A completely unique account of enumeration by Cas van der Rest and Wouter Swierstra (ICFP 2022).
• Intrinsically-typed definitional interpreters ŕ la carte by Cas van der Rest, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser, and Peter Mosses (OOPSLA 2022).
• Engineering Proof by Reflection in Agda by Paul van der Walt and Wouter Swierstra (IFL 2012).
• Internal and Observational Parametricity for Cubical Agda by Antoine Van Muylder, Andreas Nuyts, Dominique Devriese (POPL 2024).
• On Formalizing Information-Flow Control Libraries by Marco Vassena and Alejandro Russo (PLAS 2016).
• From Fine- to Coarse-Grained Dynamic Information Flow Control and Back by Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, Deian Stefan. POPL 2019 Distinguished Paper.
• Two set-based implementations of quotients in type theory by Niccolň Veltri (SPLST 2015).
• Guarded recursion in Agda via sized types by Niccolň Veltri and Niels van der Weide (FSCD 2019).
• Formalizing π-calculus in guarded cubical Agda by Niccolň Veltri, Andrea Vezzosi (CPP 2020).
• Formalizing CCS and π-calculus in Guarded Cubical Agda by Niccolň Veltri, Andrea Vezzosi (JLAMP 2023).
• An Agda Formalization of Nonassociative Lambek Calculus and its Metatheory by Niccolň Veltri, Cheng-Syuan Wan (TABLEAUX 2025).
• A Categorical Perspective on Pattern Unification by Andrea Vezzosi and Andreas Abel (UNIF 2014).
• Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types by Andrea Vezzosi, Anders Mörtberg, and Andreas Abel (ICFP 2019).
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types by Andrea Vezzosi, Anders Mörtberg, Andreas Abel (JFP 2021).
• Structured Contracts in the EUTxO Ledger Model by Polina Vinogradova, Orestis Melkonian, Philip Wadler, Manuel Chakravarty, Jacco Krijnen, Michael Peyton Jones, James Chapman, and Tudor Ferariu (FMBC @ ETAPS 2024).

W

• Arity-Generic Datatype-Generic Programming by Stephanie Weirich and Chris Casinghino (PLPV 2010).
• Initial Algebras Unchained - A Novel Initial Algebra Construction Formalized in Agda by Thorsten Wißmann, Stefan Milius (LICS 2024).

X

• A constructive model of uniform continuity by Chuangjie Xu and M.H. Escardo, TLCA 2013.
• A Continuous Computational Interpretation of Type Theories by Chuangjie Xu, PhD thesis.

Z

• π with Leftovers: A Mechanisation in Agda by Uma Zalakain and Ornela Dardha (FORTE 2021).
• Focusing and higher-order abstract syntax by Noam Zeilberger (POPL 2008; the paper does not mention Agda, but some accompanying Agda code is available).
• Refinement Types and Computational Duality by Noam Zeilberger (PLPV 2009).
• The Functor of Points Approach to Schemes in Cubical Agda by Max Zeuner, Matthias Hutzler (ITP 2024).
• A Univalent Formalization of Constructive Affine Schemes by Max Zeuner, Anders Mörtberg (TYPES 2022).

(350 papers as of 2026-04-10.)