[Agda] HCAR report

Andreas Abel andreas.abel at ifi.lmu.de
Thu Oct 31 14:52:23 CET 2013

The Haskell communities and activities report is due tomorrow.  Enclosed 
you find a draft of the report.  If you have anything to add or correct, 
please submit a patch to me with edits of


or send corrections to me by mail before tommorrow.


\report{Andreas Abel}%11/13
\status{actively developed}
\participants{Nils Anders Danielsson, Ulf Norell, Makoto Takeyama,
Stevan Andjelkovic, Jean-Philippe Bernardy, James Chapman,
Dominique Devriese, Peter Divianszki,
Fredrik Nordvall Forsberg, Olle Frediksson, Daniel Gustafsson,
Alan Jeffrey, Fredrik Lindblad, Guilhem Moulin, Nicolas Pouillard, 
Andrés Sicard-Ramírez
and many others}

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

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.

Since the release of Agda~2.3.2 in November 2012 the following has
happened in the Agda project and community:
\item Ulf Norell gave a keynote speech at ICFP 2013 on dependently
   typed programming in Agda.
\item Agda has attracted new users, the traffic on the mailing list
   (and bug tracker) is increasing.
\item About 100 bugs of Agda~2.3.2 have been fixed; and small
   enhancements improve the usability.
\item Copatterns are being added to Agda as a new way to define record
   and coinductive values.
Release of Agda~2.3.4 is planned to happen soon after the one of GHC~7.8.

   The Agda Wiki: \url{http://wiki.portal.chalmers.se/agda/}
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: November-2013.pdf
Type: application/pdf
Size: 85731 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20131031/55aa63e7/November-2013-0001.pdf

More information about the Agda mailing list