- 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).
- 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)
- 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).
- 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).
- 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).
- 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.
- 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).
- 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.
- 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).
- 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).
- 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.
- 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).
- 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).
- 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).
- 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).
- 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).
- 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.
- 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).
- 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).
- A Categorical Perspective on Pattern Unification by Andrea Vezzosi and Andreas Abel (UNIF 2014).
- Arity-Generic Datatype-Generic Programming by Stephanie Weirich and Chris Casinghino (PLPV 2010).
- 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.
- 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.)