# 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).
- 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).
- 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
- Big-Step Normalisation by Thorsten Altkenkirch 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.
- 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).
- Observational Equality, Now! by Thorsten Altenkirch, Conor McBride and Wouter Swierstra (PLPV 2007).
- Indexed Containers by Thorsten Altenkirch and Peter Morris (LICS 2009).
- 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

- 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).
- 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).
- 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).
- 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).
- Isomorphism Is Equality by Thierry Coquand and Nils Anders Danielsson (Indagationes Mathematicae).

#### D

- 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).
- 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).
- 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
- What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common by Martin Escardó and Paulo Oliva (MSFP 2010).

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

#### G

- An Algebraic Foundation and Implementation of Induction Recursion and Indexed Induction Recursion by Neil Ghani and Peter Hancock.
- Staged Multi-Result Supercompilation: Filtering by Transformation. by Sergei Grechanik, Ilya Klyuchnikov and Sergei Romanenko (Meta 2014; slides, Agda source).

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

- 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).
- Generalizations of Hedberg’s Theorem by Nicolai Kraus, Martín Escardó, Thierry Coquand and Thorsten Altenkirch (TLCA 2013; formalised in Agda).
- The Universe U_n is not an n-type by Nicolai Kraus and Christian Sattler (formalised in Agda).

#### L

- Type-safe diff for families of datatypes by Eelco Lempsink, Sean Leather, Andres Löh (WGP 2009).
- 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).
- 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

- Small Induction Recursion, Indexed Containers and Dependent Polynomials are equivalent by Lorenzo Malatesta, Thorsten Altenkirch, Neil Ghani, Peter Hancock and Conor McBride (TLCA 2013).
- Ornamental Algebras, Algebraic Ornaments by Conor McBride.
- Outrageous but Meaningful Coincidences: Dependent type-safe syntax and evaluation by Conor McBride (WGP 2010).
- 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 Mu, Ko & Jansson (JFP 2009).
- Algebra of Programming Using Dependent Types by Mu, Ko & 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).

#### O

- The Power Of Pi by Nicolas Oury and Wouter Swierstra (ICFP 2008).

#### P

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

#### T

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

#### W

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

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