Haskell alterantives for Isabelle or ACL2

D. Tweed tweed@compsci.bristol.ac.uk
Wed, 14 May 2003 10:49:22 +0100 (BST)


On Tue, 13 May 2003, Iavor Diatchki wrote:

> hello,
> as far as i know there are no real theorem provers using haskell as a 
> metalanguage.
> there also aren't any text editors that can be programmed in haskell, i 
> wonder how many people have wanted to program their emacs in haskell :-)

Claus Reineke (if I'm remembering the attribution correctly; I often get
it embarassingly wrong) said maybe a year ago that he'd got some Haskell
scriptability for vi working.

___cheers,_dave_________________________________________________________
www.cs.bris.ac.uk/~tweed/  |  `It's no good going home to practise
email:tweed@cs.bris.ac.uk  |   a Special Outdoor Song which Has To Be
work tel:(0117) 954-5250   |   Sung In The Snow' -- Winnie the Pooh