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 16.00 - 17.00 LFCS Seminar: 5 May 2020 - Francesco Gavazzo Speaker: Francesco Gavazzo Blackboard Collaborate: Invitation only
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 16.00 - 17.00 LFCS Seminar: 5 May 2020 - Francesco Gavazzo Speaker: Francesco Gavazzo Blackboard Collaborate: Invitation only