agda/doc/HCAR/November-2011.tex

\documentclass{article}

\usepackage{hcar}

\begin{document}

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

At the time of writing version 2.3.0 is about to be released, with the
following new features (among others):
\begin{itemize}
\item Instance arguments (Dominique Devriese).
\item A JavaScript backend (Alan Jeffrey).
\item More optimizations in the Epic backend (Olle Fredriksson and
  Daniel Gustafsson).
\item Pattern matching, multi-clause lambdas (Fredrik Nordvall
  Forsberg, Karim Kanso and Noam Zeilberger).
\end{itemize}

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

\end{document}