agda/doc/HCAR/Agda-AA-Nov2013.tex

% Agda-AA.tex
\begin{hcarentry}[section,updated]{Agda}
\label{agda}
\report{Andreas Abel}%11/13
\status{actively developed}
\participants{Nils~Anders~Danielsson, Ulf~Norell, Makoto~Takeyama,
Stevan~Andjelkovic, Jean-Philippe~Bernardy, James~Chapman,
Dominique~Devriese, P\'eter~Divi\'anszky,
Fredrik~Nordvall~Forsberg, Olle~Fredriksson, Daniel~Gustafsson,
Alan~Jeffrey, Fredrik~Lindblad, Guilhem~Moulin, Nicolas~Pouillard, Andr\'es~Sicard-Ram\'irez
and many more}
\makeheader

Agda is a dependently typed functional programming language (developed
using Haskell). A central feature of Agda is inductive families,
i.e., GADTs which can be indexed by \emph{values} and not just types.
The language also supports coinductive types, parameterized modules,
and mixfix operators, and comes with an \emph{interactive}
interface---the type checker can assist you in the development of your
code.

A lot of work remains in order for Agda to become a full-fledged
programming language (good libraries, mature compilers, documentation,
etc.), but already in its current state it can provide lots of fun as
a platform for experiments in dependently typed programming.

Since the release of Agda~2.3.2 in November 2012 the following has
happened in the Agda project and community:
\begin{itemize}
\item Ulf Norell gave a keynote speech at ICFP 2013 on dependently
  typed programming in Agda.
\item Agda has attracted new users, the traffic on the mailing list
  (and bug tracker) is increasing.
\item About 100 bugs of Agda~2.3.2 have been fixed; and small
  enhancements improve the usability.
\item Copatterns are being added to Agda as a new way to define record
  and coinductive values.
\end{itemize}
Release of Agda~2.3.4 is planned to happen soon after the one of GHC~7.8.

\FurtherReading
  The Agda Wiki: \url{http://wiki.portal.chalmers.se/agda/}
\end{hcarentry}