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
(26)- scientific article; zbMATH DE number 7566075 (Why is no real title available?)
- Effectful applicative bisimilarity: monads, relators, and Howe's method
- A fibrational tale of operational logical relations: pure, effectful and differential
- An internal language for categories enriched over generalised metric spaces
- A point-free perspective on lax extensions and predicate liftings
- Divergences on monads for relational program logics
- Kantorovich functors and characteristic logics for behavioural distances
- A quantified coalgebraic van Benthem theorem
- Metric reasoning about -terms: the general case
- scientific article; zbMATH DE number 5547974 (Why is no real title available?)
- On bisimilarity in lambda calculi with continuous probabilistic choice
- Combining algebraic effect descriptions using the tensor of complete lattices
- Quantitative logics for equivalence of effectful programs
- A semantic account of metric preservation
- Robustness in metric spaces over continuous quantales and the Hausdorff-Smyth monad
- Differential logical relations. I: The simply-typed case
- The syntactic side of autonomous categories enriched over generalised metric spaces
- Quantitative equality in substructural logic via Lipschitz doctrines
- 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
- Differential logical relations. II: Increments and derivatives
- Logical foundations of quantitative equality
- The lambda calculus is quantifiable
- Approximation, solution operators and quantale-valued metrics
- scientific article; zbMATH DE number 7453165 (Why is no real title available?)
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)
