Interactive Editing and Checking of Computer Programs and Their Proofs
The aim of the SIMPLE project is to design a formal language for writing program specifications, programs, and proofs that programs meet their specifications. Furthermore, I am designing a checker that will examine SIMPLE documents to check that the proofs are correct and an editor that will help the user to compose SIMPLE documents and provide an interactive interface to the checker. We take the point of view that programs are mathematical objects and thus proofs of programs are simply mathematical proofs. The SIMPLE editor and checker can handle proofs in various areas of mathematics, but are designed especially to support programming.
30 Nov -0001
Faculty of Engineering & Applied Science
St. John's, NL
Electrical and Computer Engineering
Strategic Research Theme
Information and Communication Technology