A generic complete dynamic logic for reasoning about purity and effects

DOI10.1007/s00165-010-0153-4zbMath1209.68084OpenAlexW3013099007WikidataQ130884288 ScholiaQ130884288MaRDI QIDQ973056

Lutz Schröder, Till Mossakowski, Sergei S. Goncharov

Publication date: 28 May 2010

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-010-0153-4

zbMATH Keywords

completenessdynamic logicobservational equivalencemonads for effects

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Related Items (2)

Notions of Bidirectional Computation and Entangled State Monads ⋮ A generic complete dynamic logic for reasoning about purity and effects

Uses Software

• HasCasl
• Haskell
• Eiffel
• JML
• LOOP
• Ruby
• Sather

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Notions of computation and monads
• Observational purity and encapsulation
• A generic complete dynamic logic for reasoning about purity and effects
• Coalgebras and monads in the semantics of Java
• Contracts for higher-order functions
• Side effects and aliasing can have simple axiomatic descriptions
• Computational types from a logical perspective
• Hoare logic for Java in Isabelle/HOL
• Monad-independent Dynamic Logic in HasCasl
• Algebraic Methodology and Software Technology
• Algebraic Methodology and Software Technology
• Algebra and Coalgebra in Computer Science
• An axiomatic basis for computer programming
• Completeness of Global Evaluation Logic

This page was built for publication: A generic complete dynamic logic for reasoning about purity and effects