agda/doc/user-manual/team.rst

.. _team:

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
* Matthew Daggitt
* Nils Anders Danielsson
* Ulf Norell
* Andrés Sicard-Ramírez
* Andrea Vezzosi

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, erasure*
* Guillaume Allais: *warnings, pattern guards, standard library 1.0 and above*
* 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 and above*
* Nils Anders Danielsson: *efficient positivity checker, HTML backend, highlighting, standard library*, ``--erased-cubical``
* Dominique Devriese: ``instance`` *arguments*
* Péter Diviánszky: *web frontent,* ``variable`` *declarations*
* Robert Estelle: *refactoring of backends, main driver*
* 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*
* Jonathan Prieto: *Agda package manager*
* 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, Guarded Cubical Agda*
* Noam Zeilberger: *pattern lambdas*
* Tesla Ice Zhang

The full list of code and documentation contributors (more than 170)
is available at https://github.com/agda/agda/graphs/contributors
or from the git repository via ``git shortlog -sne``.
Numerous further individuals have contributed to Agda by reporting
issues, building backends and editor support, packaging Agda etc.

The Agda license is `here
<https://github.com/agda/agda/blob/master/LICENSE>`_.