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.
- Myreen, Magnus O.; Davis, Jared: A verified runtime for a verified theorem prover (2011)
- 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)
- Barthe, Gilles; Grégoire, Benjamin; Kunz, César; Rezk, Tamara: Certificate translation for optimizing compilers (2006)
- Lerner, Sorin; Millstein, Todd D.; Chambers, Craig: Cobalt: A language for writing provably-sound compiler optimizations. (2005)
- Salcianu, Alexandru; Arkoudas, Konstantine: Machine-checkable correctness proofs for intra-procedural dataflow analyses. (2005)
- 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)