Browsing by Author "Simpson, Todd"
Now showing 1 - 3 of 3
Results Per Page
Sort Options
- ItemOpen AccessCORRECTNESS OF A COMPILER SPECIFICATION FOR THE SECD MACHINE(1990-10-01) Simpson, ToddWe develop a specification in Natural Semantics of a compiler from the lambda calculus with let and letrec (miniSML) to the SECD machine. We prove that the compiler specification is correct by simplifying the approach of Despeyroux [2] and changing the proof technique to work with non-terminating semantics. We then extend the SECD to handle lazy evaluation and outline the proof of the compiler specification for this.
- ItemOpen AccessIFL: AN INTERMEDIATE CODE FOR FUNCTIONAL LANGUAGES(1989-01-01) Simpson, ToddFunctional Languages all share the lambda calculus as a common basis. Existing intermediate functional languages are simple extensions of the lambda calculus to include let and letrec constructs. This paper proposes a more extensive intermediate language which supports simple data types, pattern matching, and interactive environments. Motivation, design considerations, semantics, and progress to date are included.
- ItemOpen AccessSOME STEPS TOWARDS A VERIFIED SYSTEM(1992-02-01) Birtwistle, G.; Simpson, Todd; Graham, BrianA totally verified system consists of a meaning preserving compiler and hardware which correctly interprets the resulting machine code. This paper describes work in progress towards this goal using MiniSML, a small functional language, and the SECD machine. A functional language is used to ease software proofs, and the SECD machine was chosen as it was the best documented machine when we began this work. This paper outlines a (hand) proof of the correctness of a translator from MiniSML to SECD machine code and a mechanized HOL proof of the hardware which realizes the abstract SECD machine. To achieve a totally verified system, further work is required to mechanize the translator proof and tie it directly to the machine proof, and to recognize the constraints of the machine (i.e., memory capacity) at the software level.