coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ANN: MiniAgda-0.2014.1.9 Toy language with dependent and sized types

From: Andreas Abel <andreas.abel AT ifi.lmu.de>
To: haskell-cafe <haskell-cafe AT haskell.org>, Agda List <agda AT lists.chalmers.se>, coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] ANN: MiniAgda-0.2014.1.9 Toy language with dependent and sized types
Date: Thu, 09 Jan 2014 19:39:43 +0100

For what it's worth, I finally uploaded MiniAgda to hackage. If you want to play around with type-based termination and coinduction in a dependently-typed setting, try:

cabal install MiniAgda

Some examples and pointers to literature are (still) on my old homepage:

http://www2.tcs.ifi.lmu.de/~abel/miniagda/

Source code and issue tracker are on the darcs hub:

http://hub.darcs.net/abel/miniagda/

Have fun playing (or despair of the horrible error messages),
and have a happy new year,

Andreas

--
Andreas Abel <>< Du bist der geliebte Mensch.

[Coq-Club] ANN: MiniAgda-0.2014.1.9 Toy language with dependent and sized types, Andreas Abel, 01/09/2014
- Re: [Coq-Club] [Agda] ANN: MiniAgda-0.2014.1.9 Toy language with dependent and sized types, gallais, 01/10/2014