LFCS Seminar: 5 May 2020 - Francesco Gavazzo

Title:  Operational reasoning for modal types: effects and coeffects 

Abstract:

In this talk, I will present some ongoing work on operationally-based, coinductive notions of program equivalence for higher-order languages with effects and coeffects. The first part of the talk will focus on notions of applicative bisimulation for languages with algebraic effects and monadic types, with special attention to their extensionsto graded monadic type systems. 

The second part of the talk will deal with program equivalence for effectful and coeffectful languages, the latter being modelled relying on the notions of a graded comonadic type system. In particular, a 'resource-sensitive' refinement of the notion of an applicative bisimulation presented in the first part of the talk will be analysed.

Affiliation:

University of Bologna

May 05 2020 -

LFCS Seminar: 5 May 2020 - Francesco Gavazzo

Speaker: Francesco Gavazzo

Blackboard Collaborate:
Invitation only