- 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).
Papers using Agda
List of papers sorted by name of first author:
- 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).
- 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).
- 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).
- 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).
- 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).
- 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).
- 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).
- 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).
- 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).
- 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).
- 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).
- 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).
- 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).
- 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).
- The Power Of Pi by Nicolas Oury and Wouter Swierstra (ICFP 2008).
- 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).
- 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.
- Agda Meets Accelerate by Peter Thiemann and Manuel M. T. Chakravarty (IFL 2012).
- Coherence for skew-monoidal categories by Tarmo Uustalu (MSFP 2014).
- Engineering Proof by Reflection in Agda by Paul van der Walt and Wouter Swierstra (IFL 2012).
- Arity-Generic Datatype-Generic Programming by Stephanie Weirich and Chris Casinghino (PLPV 2010).