The Coq mailing list

[David Nowak <David.Nowak AT lsv.ens-cachan.fr>]

Thery Laurent wrote:
> I've an exact correctness proof of the unification algorithm given by 
> John Harrison
>
> http://www.cl.cam.ac.uk/users/jrh/atp/index.html
>
> It is exact in the sense that the extracted code is as close as possible
> to John's implementation (unfortunately it can't be exactly the same 
> since John is using exceptions).

What about using exception monad? Could you then extract an exact 
call-by-value translation of the algorithm?

More generally are there development in Coq using monad to deal with 
side effects?

David.

--
David Nowak
LSV, CNRS UMR 8643 & ENS de Cachan
61, av. du President Wilson, 94235 Cachan Cedex, France
tel: +33 1 47 40 75 47   fax: +33 1 47 40 75 21
http://www.lsv.ens-cachan.fr/~nowak/