VLISP
VLISP refers to at least three distinct items.These are, in no particular order:A Lisp dialect implemented and formalized since 1971 at the University of Paris VIII - Vincennes, France. VLISP (for Vincennes LISP) interpreters and compilers were designed to run on small machines and were extremely fast. This VLISP led to Le-Lisp.A formally verified implementation of the Scheme programming language (Scheme is a dialect of Lisp).The ”Visual Lisp” implementation included in recent versions of AutoCAD.
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
Sorted by year (- Myreen, Magnus O.; Davis, Jared: A verified runtime for a verified theorem prover (2011)
- Benton, Nick; Hur, Chung-Kil: Biorthogonality, step-indexing and compiler correctness (2009)
- Leroy, Xavier: A formally verified compiler back-end (2009)
- Myreen, Magnus O.; Gordon, Michael J. C.: Verified LISP implementations on ARM, x86 and PowerPC (2009) ioport
- Barthe, Gilles; Grégoire, Benjamin; Kunz, César; Rezk, Tamara: Certificate translation for optimizing compilers (2006)
- van Engelen, Robert; Whalley, David; Yuan, Xin: Automatic validation of code-improving transformations on low-level program representations (2004)
- Guttman, Joshua D. (ed.); Wand, Mitchell (ed.): VLISP. A verified implementation of scheme (1995)
- Guttman, Joshua D.; Ramsdell, John D.; Wand, Mitchell: VLISP: A verified implementation of scheme. (1995) ioport