agda/doc/HCAR/May-2013.tex

\documentclass{article}

\usepackage{hcar}

\begin{document}

% Agda-NA.tex
\begin{hcarentry}[section,updated]{Agda}
\label{agda}
\report{Nils Anders Danielsson}%05/13
\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.

In November Agda~2.3.2 was released, with the following changes (among
others):
\begin{itemize}
\item Pattern synonyms (Stevan Andjelkovic and Adam Gundry).
\item Modifications to the constraint solver (Andreas Abel).
\item A \LaTeX\ backend, with the aim to support both precise,
  Agda-style highlighting, and lhs2TeX-style alignment of code (Stevan
  Andjelkovic).
\item The Emacs mode no longer depends on GHCi and haskell-mode (Peter
  Divianszky).
\item The Emacs mode is more interactive: type-checking no longer
  blocks Emacs, and there is an option to highlight the expression
  that is currently being type-checked (Guilhem Moulin and Nils Anders
  Danielsson).
\end{itemize}

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

\end{document}