agda/doc/HCAR/May-2012.tex

\documentclass{article}

\usepackage{hcar}

\begin{document}

% Agda-NA.tex
\begin{hcarentry}[section,updated]{Agda}
\label{agda}
\report{Nils Anders Danielsson}%05/12
\status{actively developed}
\participants{Ulf Norell, Andreas Abel, 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.

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.

The next version of Agda is under development. The most interesting
changes to the language may be the addition of pattern synonyms,
contributed by Stevan Andjelkovic and Adam Gundry, and modifications
of the constraint solver, implemented by Andreas Abel. Other work has
targeted the Emacs mode. Peter Divianszky has removed the prior
dependency on GHCi and haskell-mode, and Guilhem Moulin and myself
have made the Emacs mode more interactive: type-checking no longer
blocks Emacs, and the expression that is currently being type-checked
is highlighted.

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

\end{document}