Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances - Archive ouverte HAL Access content directly
Conference Papers Year :

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

(1, 2)
1
2

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.
Fichier principal
Vignette du fichier
lics2018CameraReady.pdf (805.08 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01926069 , version 1 (18-11-2018)

Identifiers

Cite

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⟩
20 View
102 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More