Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances

Author: Francesco Gavazzo

Paper Information

Title:Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
Authors:Francesco Gavazzo
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:applicative simulation distance, applicative bisimulation distance, effectful bisimilarity, algebraic effects, fuzz, quantale relator, howe's method

ABSTRACT. This paper studies the quantitative refinement of Absramsky's applicative similarity and bisimilarity in the context of a generalisation of Fuzz, a call-by-value $\lambda$-calculus with a linear type system that can express program sensitivity, enriched with algebraic operations \emph{\`a la} Plotkin and Power. To do so a general, abstract framework for studying behavioural relations taking values over quantales is defined according to Lawvere's analysis of generalised metric spaces. Barr's notion of relator (or lax extension) is then extended to quantale-valued relations adapting and extending results from the field of monoidal topology. Abstract notions of quantale-valued effectful applicative similarity and bisimilarity are then defined and proved to be a compatible generalised metric (in the sense of Lawvere) and pseudometric, respectively, under mild conditions.

Talk:Jul 12 09:00 (Session 70E)