20 października 2016 14:00
Filip Sieczkowski: Step-Indexed Kripke Models over Recursive Worlds
Over the last two decades, significant progress has been made in modelling certain sophisticated features of programming languages and program logics. Perhaps the most crucial of these are higher-order store and storable assertions/resource invariants. One of the more general lines of solutions to these problems features Kripke models over worlds that are recursively defined in appropriate rich categories. This technique originated in the denotational world, but has since been generalised, and remains quite widely used.
In this talk, I would like to give an in-depth account of the problems raised by the presence of higher-order state, and present a way to overcome these, in a simple operational setting, by using Kripke models over worlds recursively defined in the universe of metric spaces. The presentation will mostly follow Birkedal et al.'s POPL'11 paper under the same title.