On Fri, 28 Sep 2007, Jeff Polakow <[EMAIL PROTECTED]> wrote: > Agda is essentially an implementation of a type checker for > Martin-Lof type theory (i.e. dependent types). > > It is designed to be used as a proof assistant.
Well, the language aims to become a practical programming language. Ulf's recently defended PhD thesis has the title "Towards a practical programming language based on dependent type theory" (http://www.cs.chalmers.se/~ulfn/papers/thesis.html). Lots of work remains to be done before this goal is reached, though. In the meantime, Agda is an excellent vehicle for experiments in dependently typed programming with inductive families (≈ GADTs). For more information, see the Agda wiki (http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php). -- /NAD _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
