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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

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

Cited in

(11)

• Trace-Based Coinductive Operational Semantics for While
• A metalanguage for guarded iteration
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• Automated temporal verification for algebraic effects
• Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction
• A Hoare logic for the coinductive trace-based big-step semantics of While
• A dynamic logic with traces and coinduction
• scientific article; zbMATH DE number 7199590 (Why is no real title available?)
• Leaving Traces: A Note on a Sound and Complete Trace Logic for Concurrent Constraint Programs
• Into the Infinite - Theory Exploration for Coinduction
• scientific article; zbMATH DE number 7080198 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

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)