agda/doc/HCAR/November-2012.tex

\documentclass{article}

\usepackage{hcar}

\begin{document}

% Agda-NA.tex
\begin{hcarentry}[section,updated]{Agda}
\label{agda}
\report{Nils Anders Danielsson}%11/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 still under development. Some of the
changes were mentioned in the last HCAR entry. More recently Stevan
Andjelkovic has contributed a \LaTeX\ backend, with the aim to support
both precise, Agda-style highlighting, and lhs2TeX-style alignment of
code.

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

\end{document}