November 29, 2018
Ignacio Fábregas
In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources, i.e., state transition systems, to describe the invariants on the state and their allowed atomic changes. One of this logical frameworks is FCSL, developed by Aleksandar Nanevski et al. As usual, once we have a mathematical structure, it is only natural to study the functions that preserve them. This motivates the interest of defining and studying a morphism between resources. In this talk we will give an introduction to the main concepts of FCSL and the notion of resource morphism. We will also show how to apply morphisms to facilitate proof reuse between resources.