VLISP: A Verified Implementation of Scheme

VLISP: A Verified Implementation of Scheme

1995 | JOSHUA D. GUTTMAN, JOHN D. RAMSDELL, MITCHELL WAND
The VLISP project, led by Joshua D. Guttman, John D. Ramsdell, and Mitchell Wand, has successfully developed a verified implementation of the Scheme programming language. The project includes a rigorously verified compiler from Scheme to byte codes and a verified interpreter for the resulting byte codes. The correctness of the compiler is primarily based on the official denotational semantics for Scheme, with the Wand-Clinger technique used to prove the correctness of the primary compiler step. The operational semantics are then proven to be faithful to the denotational semantics, and the remainder of the implementation is verified through a series of state machine refinement proofs, including proofs about garbage collection. Additionally, the project includes a verified PreScheme compiler, which is the implementation language for the VLISP run-time system. This compiler is divided into three parts: a transformational front end, a syntax-directed compiler, and a linearizer. Each part uses different proof techniques, and the careful definition of the semantics of VLISP PreScheme ensures the correctness and efficiency of the compiler. The architecture and correctness proof of the PreScheme compiler can be applied to other languages as well.The VLISP project, led by Joshua D. Guttman, John D. Ramsdell, and Mitchell Wand, has successfully developed a verified implementation of the Scheme programming language. The project includes a rigorously verified compiler from Scheme to byte codes and a verified interpreter for the resulting byte codes. The correctness of the compiler is primarily based on the official denotational semantics for Scheme, with the Wand-Clinger technique used to prove the correctness of the primary compiler step. The operational semantics are then proven to be faithful to the denotational semantics, and the remainder of the implementation is verified through a series of state machine refinement proofs, including proofs about garbage collection. Additionally, the project includes a verified PreScheme compiler, which is the implementation language for the VLISP run-time system. This compiler is divided into three parts: a transformational front end, a syntax-directed compiler, and a linearizer. Each part uses different proof techniques, and the careful definition of the semantics of VLISP PreScheme ensures the correctness and efficiency of the compiler. The architecture and correctness proof of the PreScheme compiler can be applied to other languages as well.
Reach us at info@study.space
[slides and audio] Volume 8