The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes
From MaRDI portal
Publication:5277914
DOI10.1145/2835491zbMath1367.68069OpenAlexW2228757736MaRDI QIDQ5277914
Publication date: 12 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2835491
Hoare logicmonadic recursion schemespropositional Hoare logiccontext-free programsmonadic program schemessound and complete Hoare calculus
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Semantic Foundations for Deterministic Dataflow and Stream Processing ⋮ Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism ⋮ Equational Theories of Abnormal Termination Based on Kleene Algebra
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Ten years of Hoare's logic: A survey. II: Nondeterminism
- Equivalence problems for deterministic context-free languages and monadic recursion schemes
- Propositional dynamic logic of regular programs
- A completeness theorem for Kleene algebras and the algebra of regular events
- Program schemes, recursion schemes, and formal languages
- On the completeness of propositional Hoare logic
- \(L(A)=L(B)\)? A simplified decidability proof.
- Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism
- Kleene Algebra with Products and Iteration Theories
- Decidability of DPDA Language Equivalence via First-Order Grammars
- Language Equivalence of Deterministic Real-Time One-Counter Automata Is NL-Complete
- Ten Years of Hoare's Logic: A Survey—Part I
- Alternation
- Soundness and Completeness of an Axiom System for Program Verification
- The equivalence problem for deterministic pushdown automata is decidable
- Infinitary Axiomatization of the Equational Theory of Context-Free Languages
- Recursive Unsolvability of a problem of Thue
- Kleene Algebra with Equations
- NetKAT
- Equivalences of Pushdown Systems Are Hard
- Equivalence of deterministic one-counter automata is NL-complete
- Deterministic context free languages
- An axiomatic basis for computer programming
- On Hoare logic and Kleene algebra with tests
- A note on the complexity of propositional Hoare logic
