Abstract:
Modern compilers not only convert programs to a lower-level representation, such as machine code, but also optimize programs to make them more efficient. Proving that such optimizations do not affect the results of a program is a challenging task. One of the methods that addresses such proofs is modeling a programming language in a formal system, often called a calculus, and using operational semantics to represent a program's evaluation.
In this talk I will introduce two systems for modeling programs and their transformations: the lambda calculus, a well known system for modeling functions, and its extension - a calculus of records which is used to model program modules. I will discuss properties of the calculi that allow us to prove that a certain class of program transformations preserve the behavior of a program. I will present two approaches to such proof: a method based on properties called confluence and standardization, which is suitable for the lambda calculus, and a method based on properties called lift and project that we developed for the calculus of records which lacks the confluence property.
This is joint work with Franklyn Turbak, Wellesley College, USA.