A sound and complete logic for algebraic effects

DOI10.1007/978-3-030-17127-8_22MaRDI QIDQ2289090zbMATH OpenOpenAlexFDO

Authors Cristina Matache, Sam Staton

Publication date 28 January 2020

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-17127-8_22

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Recommendations

• Behavioural equivalence via modalities for algebraic effects
• Quantitative logics for equivalence of effectful programs
• scientific article; zbMATH DE number 7453165
• An effect system for algebraic effects and handlers
• scientific article; zbMATH DE number 1705158

Cited in

(10)

• Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation
• Runners for interleaving algebraic effects
• A complete axiomatisation for the logic of lattice effect algebras
• Combining algebraic effect descriptions using the tensor of complete lattices
• Behavioural equivalence via modalities for algebraic effects
• A complete normal-form bisimilarity for algebraic effects and handlers
• Efficient algebraic effect handlers for Prolog
• Effect polymorphism in higher-order logic (proof pearl)
• Inductive and coinductive predicate liftings for effectful programs
• scientific article; zbMATH DE number 7453165 (Why is no real title available?)

This page was built for publication: A sound and complete logic for algebraic effects

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