agda/doc/HCAR/November-2018.tex

% Agda-UA.tex
\begin{hcarentry}[updated]{Agda}
\label{agda}
\report{Ulf Norell}%11/18
\status{actively developed}
\participants{Ulf Norell, Nils Anders Danielsson, Andreas Abel,
Jesper Cockx, 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 others}
\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.

While Agda is not yet an industrial strength language, it can nevertheless
offer a lot of value as a platform for research and adventures in
dependently typed programming.

Agda~2.5.4 was released summer 2018 with a number of new features:
\begin{compactitem}
\item {\tt do}-notation
\item Compile-time call-by-need evaluation
\item Builtin 64-bit words
\item Improved performance of compiled code
\end{compactitem}

The release of Agda~2.6.0 is planned for December 2018, including
\begin{compactitem}
\item Support for Cubical Type Theory
\item Implicit forall-generalization
\item Prop: a universe of proof irrelevant propositions
\end{compactitem}

\FurtherReading
\begin{compactitem}
\item The Agda Wiki: \url{http://wiki.portal.chalmers.se/agda/}
\item Language reference: \url{https://agda.readthedocs.io/en/latest/language/index.html}
\end{compactitem}
\end{hcarentry}