A Hoare logic for the coinductive trace-based big-step semantics of While
DOI10.1007/978-3-642-11957-6_26zbMATH Open1260.68111OpenAlexW1480120842MaRDI QIDQ3558243FDOQ3558243
Authors: Keiko Nakata, Tarmo Uustalu 
Publication date: 4 May 2010
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-11957-6_26
Recommendations
- A Hoare logic for the coinductive trace-based big-step semantics of While
- Trace-Based Coinductive Operational Semantics for While
- A dynamic logic with traces and coinduction
- Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction
- Programming Languages and Systems
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)
Cited In (11)
- A Hoare logic for the coinductive trace-based big-step semantics of While
- Into the Infinite - Theory Exploration for Coinduction
- Leaving Traces: A Note on a Sound and Complete Trace Logic for Concurrent Constraint Programs
- Title not available (Why is that?)
- Characteristic formulae for liveness properties of non-terminating CakeML programs
- Automated temporal verification for algebraic effects
- A metalanguage for guarded iteration
- Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction
- Title not available (Why is that?)
- Trace-Based Coinductive Operational Semantics for While
- A dynamic logic with traces and coinduction
Uses Software
This page was built for publication: A Hoare logic for the coinductive trace-based big-step semantics of While
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3558243)
