I think VLISP is, as well. VLISP (not the French one from the 80s, the other one, though the French one was interesting in its own right [1]), was a verified Scheme implementation written in a verified version of Pre-Scheme. Sweet research project, but I haven't seen any public releases of it :/
VLISP was a precursor to Le-Lisp [2], which was massively popular and influential in Europe, and could run faster on commodity hardware than Lisp Machine Lisp on the Symbolics 3600.
[2]: http://lelisp.org/ (under construction, but with some useful links for the time being).
France was actually a hotbed of Lisp across the pond and, along with the UK, pretty invested in a European standard for Lisp, first EuLisp (which was an excellent language but somehow flopped unfortunately) and ISLISP (an ISO standard that's not so excellent -- basically a crippled version of Common Lisp -- and also pretty much flopped). I've been in talks with some of the Le-Lisp guys about the possibility of open-sourcing Le-Lisp now that it's no longer commercially viable -- fingers crossed! :)
P.S., if anyone from INRIA happens to be reading this: pretty please?? Jérôme agrees! :)
I think VLISP is, as well. VLISP (not the French one from the 80s, the other one, though the French one was interesting in its own right [1]), was a verified Scheme implementation written in a verified version of Pre-Scheme. Sweet research project, but I haven't seen any public releases of it :/
There are some papers about both here: http://library.readscheme.org/page8.html
[1]: http://www.artinfo-musinfo.org/en/issues/vlisp/index.html
VLISP was a precursor to Le-Lisp [2], which was massively popular and influential in Europe, and could run faster on commodity hardware than Lisp Machine Lisp on the Symbolics 3600.
[2]: http://lelisp.org/ (under construction, but with some useful links for the time being).
France was actually a hotbed of Lisp across the pond and, along with the UK, pretty invested in a European standard for Lisp, first EuLisp (which was an excellent language but somehow flopped unfortunately) and ISLISP (an ISO standard that's not so excellent -- basically a crippled version of Common Lisp -- and also pretty much flopped). I've been in talks with some of the Le-Lisp guys about the possibility of open-sourcing Le-Lisp now that it's no longer commercially viable -- fingers crossed! :)
P.S., if anyone from INRIA happens to be reading this: pretty please?? Jérôme agrees! :)