A Verified Compiler for Multithreaded PreScheme William M. Farmer, John D. Ramsdell 1996 Abstract Multithreaded PreScheme is a systems programming language for high-assurance systems. It is based on VLISP PreScheme, a systems programming language dialect of Scheme developed by the VLISP project. Multithreaded PreScheme is an extension of VLISP PreScheme which allows programs with more than one thread of control. This document describes the language and also a verified compiler which generates code for MIPS-based architectures. The two major contributions described in this report are a proof of the correctness of code generated for execution in the presence of multiple threads, and a new code generator that produces substantially faster code than that produced by the verified complier for VLISP PreScheme.