LFCS Seminar: Tuesday, 10 October - Koko Muroya


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




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.











Oct 10 2023 -

LFCS Seminar: Tuesday, 10 October - Koko Muroya

Koko Muroya, Kyoto University https://www.kurims.kyoto-u.ac.jp/~kmuroya/

Venue: Mini Forum 2, IF4.40