# Publications

## Getting Started

- Download.
- Language tutorials.
- Quick guide to editing, type checking and compiling Agda code.
- Community: mailing list and IRC channel. Don’t hesitate to ask questions!

## Documentation and examples

- Manuals and howtos.
- Standard library, and other libraries and developments (all Agda users are strongly encouraged to add their own developments to make them available to the community).

## Courses using Agda

## Papers using Agda

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).
- When Is a Container a Comonad? by Danel Ahman, James Chapman and Tarmo Uustalu (FoSSaCS 2012).
- 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 (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
- Type and Scope Preserving Semantics by Guillaume Allais, James Chapman, and Conor McBride
- 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).
- Partiality, Revisited by Thorsten Altenkirch and Nils Anders Danielsson (extended abstract for TYPES 2016 talk; Agda formalisation).
- Termination Checking in the Presence of Nested Inductive and Coinductive Types by Thorsten Altenkirch and Nils Anders Danielsson.
- 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).
- 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 Type Theoretic Specification of Partial Evaluation by Kenichi Asai, Luminous Fennell, Peter Thiemann and Yang Zhang (PPDP 2014)

#### B

- 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.
- 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)
- 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).
- 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).
- Quotienting the delay monad by weak bisimilarity by James Chapman, Tarmo Uustalu, Niccolò Veltri (ICTAC 2015).
- Formal derivation of greedy algorithms from relational specifications: A tutorial by Yu-Hsi Chiang and Shin-Cheng Mu (JLAMP, in press).
- 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 (submitted to 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).
- 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 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).
- Veriﬁed 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).

#### 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).
- 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).
- Staged Multi-Result Supercompilation: Filtering by Transformation. by Sergei Grechanik, Ilya Klyuchnikov and Sergei Romanenko (Meta 2014; slides, Agda source).
- 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).
- 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

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

#### 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

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

- Embedding Polymorphic Dynamic Typing by Thomas van Noort, Wouter Swierstra, Peter Achten, Rinus Plasmeijer (WGP 2011).
- 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).

#### O

- Using session types as an effect system by Dominic Orchard and Nobuko Yoshida (PLACES 2015; Agda formalisation).
- 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

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

#### U

- Coherence for skew-monoidal categories by Tarmo Uustalu (MSFP 2014).

#### V

- Engineering Proof by Reflection in Agda by Paul van der Walt and Wouter Swierstra (IFL 2012).
- A Categorical Perspective on Pattern Unification by Andrea Vezzosi and Andreas Abel (UNIF 2014).

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

(188 papers as of 2016–05–12.)