Publications

Getting Started

• Install Agda on your own PC or try out Agda in the browser with the Agda Pad.
• Get your feet wet with A Taste of Agda.
• Read one of the language tutorials.
• Ask any questions on the Agda mailing list or on the Agda Zulip server.

Courses using Agda

Papers using Agda

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).
• Decidability of Conversion for Type Theory in Type Theory by Andreas Abel, Joakim Öhman, and Andrea Vezzosi (POPL 2018).
• A Formalized Proof of Strong Normalization for Guarded Recursive Types by Andreas Abel and Andrea Vezzosi (APLAS 2014).
• Normalization by evaluation for sized dependent types by Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (ICFP 2017).
• 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)
• Type-preserving compilation via dependently typed syntax by Andreas Abel (TYPES 2020)
• 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).
• Non-wellfounded trees in Homotopy Type Theory by Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti (TLCA 2015)
• Mechanised Relation-Algebraic Order Theory in Ordered Categories without Meets by Musa Al-hassy and Wolfram Kahl, RAMICS 2014.
• 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).
• 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).

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).
• 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).

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
• Sikkel: Multimode Simple Type Theory as an Agda Library by Joris Ceulemans, Andreas Nuyts, Dominique Devriese (MSFP 2022).
• 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).
• Fractional Types: Expressive and Safe Space Management for Ancilla Bits by Chao-Hong Chen, Vikraman Choudhury, Jacques Carette, Amr Sabry
• 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)
• 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)
• 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).
• 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)
• 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.
• 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

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
• 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.

F

• 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

• 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).
• 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)
• 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).

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.
• Hereditary Substitutions for Simple Types, Formalized by Chantal Keller and Thorsten Altenkirch (MSFP 2010).
• On the Agda Language (in Japanese) by Yoshiki Kinoshita.
• Category Theoretic Structure of Setoids by Yoshiki Kinoshita and John Power (TCS).
• 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
• Formalising type-logical grammars in Agda by Pepijn Kokke (TYTLES).
• Auto in Agda: programming proof search using reflection by Pepijn Kokke and Wouter Swierstra (MPC 2015).
• Intrinsic Verification of a Regular Expression Matcher by Joomy Korkut, Maksim Trifunovski and Daniel R. Licata.
• 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

• 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).
• 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).
• 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
• Clock Constraints Specification Langage : A mechanized denotational semantics in Agda by Mathieu Montin, Marc Pantel.
• Security-Typed Programming within Dependently-Typed Programming by Jamie Morgenstern and Daniel R. Licata (ICFP 2010).
• 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).
• 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
• 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

• 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).

Q

R

• Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages by Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser (CPP 2020)

S

• 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)
• Constructive Provability Logic by Robert J. Simmons and Bernardo Toninho (presented at IMLA 2011).
• 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.
• 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).
• From algebra to abstract machine: a verified generic construction by Carlos Tomé Cortiñas and Wouter Swierstra (TyDe 2018).

U

• 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

• 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).
• 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).

W

• Arity-Generic Datatype-Generic Programming by Stephanie Weirich and Chris Casinghino (PLPV 2010).

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

• 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).

(235 papers as of 2020-02-22.)