rappel: séminaire PPS c'est à 11h en salle 1D23 (café a 10.45)

Bonjour à tous et toutes

Le séminaire PPS c'est dans quelques instants !
Nous écouterons aujourd'hui Vasileios Koutavas (univ. 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.

 

Séminaire PPS: Vasileios Koutavas (Dublin) Jeudi 15/12 à 11h en salle 1D23

Bonjour,
Jeudi prochain nous accueillerons V. Koutavas, de l'université de Dublin, qui donnera son exposé en salle 1D23.
Comme d'habitude le séminaire sera précédé d'un pot informel avec café et croissants à partir de 10h45.

A bientôt
Jean

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.