Effectful applicative bisimilarity: monads, relators, and Howe's method

Authors Ugo Dal Lago, Francesco Gavazzo, Paul Blain Levy

Publication date 19 January 2021

Full work available at URL https://arxiv.org/abs/1704.04647, http://dl.acm.org/citation.cfm?id=3330052

Functional programming and lambda calculus (68N18) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

Effectful applicative similarity for call-by-name lambda calculi
Infinitary Howe's method
On applicative similarity, sequentiality, and full abstraction
On probabilistic applicative bisimulation and call-by-value \(\lambda \)-calculi
Quantitative Behavioural Reasoning for Higher-order Effectful Programs

Cited in

(23)

Effectful applicative similarity for call-by-name lambda calculi
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
The untyped computational \(\lambda \)-calculus and its intersection type discipline
Complete trace models of state and control
Infinitary Howe's method
scientific article; zbMATH DE number 7453165 (Why is no real title available?)
A categorical framework for congruence of applicative bisimilarity in higher-order languages
Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular
On reduction and normalization in the computational core
Effectful normal form bisimulation
From semantics to types: the case of the imperative \(\lambda\)-calculus
Streams of approximations, equivalence of recursive effectful programs
Runners for interleaving algebraic effects
A fibrational tale of operational logical relations: pure, effectful and differential
Logical predicates in higher-order mathematical operational semantics
From semantics to types: the case of the imperative \(\lambda\)-calculus
Two guarded recursive powerdomains for applicative simulation
Inductive and coinductive predicate liftings for effectful programs
A complete normal-form bisimilarity for algebraic effects and handlers
Intersection types for a computational lambda-calculus with global state
A robust graph-based approach to observational equivalence

This page was built for publication: Effectful applicative bisimilarity: monads, relators, and Howe's method

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