Quantitative logics for equivalence of effectful programs
From MaRDI portal
Publication:2133179
DOI10.1016/j.entcs.2019.09.015OpenAlexW2996172477WikidataQ113317348 ScholiaQ113317348MaRDI QIDQ2133179
Publication date: 29 April 2022
Full work available at URL: https://arxiv.org/abs/1904.11771
probabilitybehavioural equivalencenondeterminismerroralgebraic effectsquantitative logicmodalitiesprogram equivalenceapplicative bisimilaritycall-by-push-valueeffect combinationsglobal store
Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (4)
Weakest preconditions in fibrations ⋮ Combining algebraic effect descriptions using the tensor of complete lattices ⋮ Unnamed Item ⋮ Weakest preconditions in fibrations
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Notions of computation and monads
- Call-by-push-value: Decomposing call-by-value and call-by-name
- Generic weakest precondition semantics from monads enriched with order
- A probabilistic PDL
- Metric interpretations of infinite trees and semantics of non deterministic recursive programs
- LCF considered as a programming language
- Proving congruence of bisimulation in functional programming languages
- Behavioural equivalence via modalities for algebraic effects
- Combining effects: sum and tensor
- Similarity Quotients as Final Coalgebras
- Algebraic laws for nondeterminism and concurrency
- Substitution, jumps, and algebraic effects
- Quantitative Algebraic Reasoning
- Abstraction, Refinement and Proof for Probabilistic Systems
- Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular
- Quantitative Behavioural Reasoning for Higher-order Effectful Programs
This page was built for publication: Quantitative logics for equivalence of effectful programs
