[Agda] Re: [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad)

[Dan Doel]

On Monday 24 November 2008 6:59:56 am Álvaro García Pérez wrote:
> Hi Dan,
>
> Where can I find the reference you mentioned about the Anton Setzer's
> coalgebraic syntax?

He mentioned it in a few posts here:

http://article.gmane.org/gmane.comp.lang.agda/233/
http://article.gmane.org/gmane.comp.lang.agda/239/
http://article.gmane.org/gmane.comp.lang.agda/240/

He may have some papers going into it as well (I haven't actually looked at 
any of his publications; I should).

Also, if I had to guess, I'd say that Charity:

http://pll.cpsc.ucalgary.ca/charity1/www/home.html

probably implements something very close to what he suggests, since it's based 
as closely on category theory as any language I've ever seen. Their 
corecursive function definitions use banana brackets (which is the equivalent 
of taking unfold as the primitive) instead of Setzer's style of defining the 
observations of a function, however (there are other syntactic differences, 
too, of course).

-- Dan