# 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).
- Big-Step Normalisation by Thorsten Altkenkirch and James Chapman (JFP 2009).
- 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.
- 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

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

#### E

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