LFCS Seminar: Tuesday, 10 October - Koko Muroya

Title:         A Generative Spectrum of Preorder-Constrained Simulations for Program Refinement with Effects

Abstract

We propose a notion of preorder-constrained simulation. It is parameterised by a preorder (“observation preorder”) on traces, so that it can uniformly characterise quantitative notions of program refinement for different effects, such as exception, nondeterminism and I/O. Preorder-constrained simulation is additionally parameterised by a positive number (“look-ahead bound”), and forms a generative spectrum governed by the look-ahead bound.

Preorder-constrained simulation also comes with a game-theoretic characterisation and the so-called up-to technique.