A generic complete dynamic logic for reasoning about purity and effects

DOI10.1007/S00165-010-0153-4MaRDI QIDQ973056zbMATH OpenOpenAlexWikidataFDO

Authors Till Mossakowski, Lutz Schröder, S. 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

completenessobservational equivalencedynamic logicmonads for effects

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• A sound and complete Hoare logic for dynamically-typed, object-oriented programs
• A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
• Monad-independent dynamic logic in HasCasl.
• Monad-independent Dynamic Logic in HasCasl
• A Logic for Parametric Polymorphism with Effects

Cites work

• scientific article; zbMATH DE number 1701766 (Why is no real title available?)
• scientific article; zbMATH DE number 108549 (Why is no real title available?)
• scientific article; zbMATH DE number 1231584 (Why is no real title available?)
• scientific article; zbMATH DE number 742723 (Why is no real title available?)
• scientific article; zbMATH DE number 1952947 (Why is no real title available?)
• scientific article; zbMATH DE number 1956493 (Why is no real title available?)
• scientific article; zbMATH DE number 2087428 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• A generic complete dynamic logic for reasoning about purity and effects
• Algebra and Coalgebra in Computer Science
• Algebraic Methodology and Software Technology
• Algebraic Methodology and Software Technology
• An axiomatic basis for computer programming
• Coalgebras and monads in the semantics of Java
• Completeness of Global Evaluation Logic
• Computational types from a logical perspective
• Contracts for higher-order functions
• Hoare logic for Java in Isabelle/HOL
• Monad-independent Dynamic Logic in HasCasl
• Notions of computation and monads
• Observational purity and encapsulation
• Side effects and aliasing can have simple axiomatic descriptions

Cited in

(5)

• A dynamic characterization of the pure logic of relevant implication
• A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
• Notions of bidirectional computation and entangled state monads
• Observational purity and encapsulation
• A generic complete dynamic logic for reasoning about purity and effects

Describes a project that uses

Uses Software

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

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

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