Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [38 references]  Display  Hide  Download
Contributor : Francesco Gavazzo Connect in order to contact the contributor
Submitted on : Sunday, November 18, 2018 - 10:51:15 PM
Last modification on : Friday, October 30, 2020 - 12:04:04 PM
Long-term archiving on: : Tuesday, February 19, 2019 - 1:15:05 PM


Files produced by the author(s)




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⟩



Record views


Files downloads