Vasileios Koutavas (Dublin)

Reasoning Techniques for Program Equivalence

Abstract: Contextual equivalence is a relation between program terms which guarantees that related terms can replace each other inside any arbitrary system, without changing the system behaviour. This relation reveals fundamental symmetries of program terms that abstract away from concrete syntax and illuminate the semantics of programming languages. Its implications span from programming language design to software engineering, to system security, to program verification.

To understand the essence of contextual equivalence and develop reasoning principles we need to develop a theory that can express the basic interactions between a program expression and its environment, and discover conditions that are necessary and sufficient to establish contextual equivalence, but also intuitive and useful in proofs of equivalence.

In this talk we will review some of the theories based on coinduction and see how they can be adapted to languages with sophisticated features, such as higher-order functions, state, exceptions, polymorphism, and concurrency. We will also see how contextual equivalence helped us in the design of a novel programming language feature, and discuss some of the challenges that lie ahead.