A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While

DOI10.1007/978-3-642-11957-6_26zbMath1260.68111OpenAlexW1480120842MaRDI QIDQ3558243

Tarmo Uustalu, Keiko Nakata

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

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

Related Items (8)

A Dynamic Logic with Traces and Coinduction ⋮ Unnamed Item ⋮ Into the Infinite - Theory Exploration for Coinduction ⋮ Automated temporal verification for algebraic effects ⋮ Characteristic formulae for liveness properties of non-terminating CakeML programs ⋮ Leaving Traces: A Note on a Sound and Complete Trace Logic for Concurrent Constraint Programs ⋮ A metalanguage for guarded iteration ⋮ Unnamed Item

Uses Software

• Coq

This page was built for publication: A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While