Quantitative logics for equivalence of effectful programs

DOI10.1016/J.ENTCS.2019.09.015MaRDI QIDQ2133179zbMATH OpenOpenAlexWikidataFDO

Authors Niels Voorneveld

Publication date 29 April 2022

Full work available at URL https://arxiv.org/abs/1904.11771

zbMATH Keywords

algebraic effectsapplicative bisimilaritybehavioural equivalencecall-by-push-valueeffect combinationserrorglobal storemodalitiesnondeterminismprobabilityprogram equivalencequantitative logic

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• A sound and complete logic for algebraic effects
• Quantitative Behavioural Reasoning for Higher-order Effectful Programs
• Behavioural equivalence via modalities for algebraic effects
• scientific article; zbMATH DE number 7453165
• Effectful applicative similarity for call-by-name lambda calculi

Cites work

• A probabilistic PDL
• Abstraction, Refinement and Proof for Probabilistic Systems
• Algebraic laws for nondeterminism and concurrency
• Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular
• Behavioural equivalence via modalities for algebraic effects
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Combining effects: sum and tensor
• Effectful applicative bisimilarity: monads, relators, and Howe's method
• Generic weakest precondition semantics from monads enriched with order
• scientific article; zbMATH DE number 1705158 (Why is no real title available?)
• scientific article; zbMATH DE number 4180818 (Why is no real title available?)
• scientific article; zbMATH DE number 1330441 (Why is no real title available?)
• LCF considered as a programming language
• Metric interpretations of infinite trees and semantics of non deterministic recursive programs
• Notions of computation and monads
• Proving congruence of bisimulation in functional programming languages
• Quantitative Algebraic Reasoning
• Quantitative Behavioural Reasoning for Higher-order Effectful Programs
• Similarity quotients as final coalgebras
• Substitution, jumps, and algebraic effects

Cited in

(7)

• Weakest preconditions in fibrations
• Combining algebraic effect descriptions using the tensor of complete lattices
• A sound and complete logic for algebraic effects
• scientific article; zbMATH DE number 7453165 (Why is no real title available?)
• Weakest preconditions in fibrations
• Quantitative Behavioural Reasoning for Higher-order Effectful Programs
• QMaude: quantitative specification and verification in rewriting logic

This page was built for publication: Quantitative logics for equivalence of effectful programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2133179)