Quantitative Behavioural Reasoning for Higher-order Effectful Programs
From MaRDI portal
Abstract: This paper studies the quantitative refinements of Abramsky's applicative similarity and bisimilarity in the context of a generalisation of Fuzz, a call-by-value -calculus with a linear type system that can express programs 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.
Recommendations
- Quantitative logics for equivalence of effectful programs
- Approximating and computing behavioural distances in probabilistic transition systems
- Computing abstract distances in logic programs
- Quantified logic programs, revisited
- scientific article; zbMATH DE number 3852428
- scientific article; zbMATH DE number 7633806
- A model for behavioural properties of higher-order programs
- On behavioural abstraction and behavioural satisfaction in higher-order logic
- On behavioural abstraction and behavioural satisfaction in higher-order logic
- Observable behaviors and equivalences of logic programs
Cited in
(28)- On bisimilarity in lambda calculi with continuous probabilistic choice
- Quantitative logics for equivalence of effectful programs
- Combining algebraic effect descriptions using the tensor of complete lattices
- A quantified coalgebraic van Benthem theorem
- Approximation, solution operators and quantale-valued metrics
- Differential logical relations. II: Increments and derivatives
- Metric reasoning about -terms: the general case
- scientific article; zbMATH DE number 5547974 (Why is no real title available?)
- scientific article; zbMATH DE number 7453165 (Why is no real title available?)
- Differential logical relations. I: The simply-typed case
- Characteristic logics for behavioural hemimetrics via fuzzy lax extensions
- Effectful applicative bisimilarity: monads, relators, and Howe's method
- A semantic account of metric preservation
- Kantorovich functors and characteristic logics for behavioural distances
- An internal language for categories enriched over generalised metric spaces
- Divergences on monads for relational program logics
- A point-free perspective on lax extensions and predicate liftings
- The syntactic side of autonomous categories enriched over generalised metric spaces
- A fibrational tale of operational logical relations: pure, effectful and differential
- Robustness in metric spaces over continuous quantales and the Hausdorff-Smyth monad
- Logical foundations of quantitative equality
- A complete \(\mathcal{V}\)-equational system for graded \(\lambda\)-calculus
- A partial metric semantics of higher-order types and approximate program transformations
- The relational quotient completion
- Quantitative equality in substructural logic via Lipschitz doctrines
- The lambda calculus is quantifiable
- Identity-preserving Lax extensions and where to find them
- Compact quantitative theories of convex algebras
This page was built for publication: Quantitative Behavioural Reasoning for Higher-order Effectful Programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145320)
