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: | 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. |
Pages: | 10 |
Talk: | Jul 12 09:00 (Session 70E) |
Paper: |