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

Francesco Gavazzo 1, 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : This paper studies quantitative refinements of Abramsky's applica-tive similarity and bisimilarity in the context of a generalisation of Fuzz, a call-by-value λ-calculus with a linear type system that can express program sensitivity, enriched with algebraic operations à la Plotkin and Power. To do so a general, abstract framework for studying behavioural relations taking values over quantales is introduced 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.
Complete list of metadatas

Cited literature [38 references]  Display  Hide  Download

https://hal.inria.fr/hal-01926069
Contributor : Francesco Gavazzo <>
Submitted on : Sunday, November 18, 2018 - 10:51:15 PM
Last modification on : Tuesday, November 20, 2018 - 1:18:08 AM
Long-term archiving on : Tuesday, February 19, 2019 - 1:15:05 PM

File

lics2018CameraReady.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Francesco Gavazzo. Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances. LICS '18- Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. ⟨10.1145/3209108.3209149⟩. ⟨hal-01926069⟩

Share

Metrics

Record views

31

Files downloads

42