The Agda Team and License¶
Agda 2 was originally written by Ulf Norell, partially based on code from Agda 1 by Catarina Coquand and Makoto Takeyama, and from Agdalight by Ulf Norell and Andreas Abel.
Agda 2 is currently actively developed mainly by (in alphabetical order):
- Andreas Abel
- Guillaume Allais
- Liang-Ting Chen
- Jesper Cockx
- Nils Anders Danielsson
- Víctor López Juan
- Ulf Norell
- Andrés Sicard-Ramírez
- Andrea Vezzosi
- Tesla Ice Zhang
Agda 2 has received major contributions by the following developers, amongst others. Some contributors have pioneered a feature which shall be mentioned here. But many have worked on these features for improvements and maintenance.
- Andreas Abel: termination checker, sized types, irrelevance, copatterns
- Guillaume Allais: warnings, pattern guards, standard library 1.0
- Stevan Andjelkovic: LaTeX backend
- Miëtek Bak: Agda logo
- Marcin Benke: original “Alonzo” compiler to Haskell
- Jean-Philippe Bernardy:
syntax
declarations - Guillaume Brunerie
- James Chapman
- Liang-Ting Chen: github workflows
- Jesper Cockx: rewriting, unification
--without-K
- Catarina Coquand: Agda 1
- Matthew Daggitt: standard library 1.0
- Nils Anders Danielsson: efficient positivity checker, HTML backend, highlighting, standard library
- Dominique Devriese:
instance
arguments - Péter Diviánszky: web frontent,
variable
declarations - Robert Estelle
- Olle Fredriksson: Epic compiler backend
- Paolo Giarrusso
- Adam Gundry: pattern synonyms
- Daniel Gustafsson: Epic compiler backend
- Philipp Hausmann: treeless compiler, UHC compiler backend, testsuite runner, Travis CI
- Kuen-Bang Hou “favonia”
- Patrik Jansson
- Alan Jeffrey: JavaScript compiler backend
- Wolfram Kahl
- Wen Kokke
- John Leo
- Fredrik Lindblad: Agsy proof search “Auto”
- Víctor López Juan: “tog” prototype, markdown frontend, documentation*
- Ting-Gan Lua
- Francesco Mazzoli: “tog” prototype*
- Stefan Monnier
- Guilhem Moulin: highlighting
- Fredrik Nordvall Forsberg: pattern lambdas, warnings
- Ulf Norell: Agda 2
- Nicolas Pouillard: module record expressions
- Benjamin Price
- Jonathan Prieto: Agda package manager
- Nobuo Yamashita
- Christian Sattler
- Andrés Sicard-Ramírez: Agda releases, Travis CI
- Makoto Takeyama: Agda 1, Emacs mode, “MAlonzo” compiler to Haskell, serialization
- Andrea Vezzosi: Cubical Agda, Agda-flat, Agda-parametric
- Noam Zeilberger: pattern lambdas
- Tesla Ice Zhang
The full list of contributors (more than 140) is available at https://github.com/agda/agda/graphs/contributors .
The Agda license is here.