A Hoare logic for the coinductive trace-based big-step semantics of While

DOI10.2168/LMCS-11(1:1)2015zbMath1448.68281arXiv1412.6579OpenAlexW2399029393MaRDI QIDQ5174911

Keiko Nakata, Tarmo Uustalu

Publication date: 19 February 2015

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1412.6579

zbMATH Keywords

nonterminationHoare logicformalizationbig-step semanticscoinductive traces

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 (3)

A Dynamic Logic with Traces and Coinduction ⋮ Unifying Guarded and Unguarded Iteration ⋮ A metalanguage for guarded iteration

Uses Software

• Coq

This page was built for publication: A Hoare logic for the coinductive trace-based big-step semantics of While