Trace-Based Coinductive Operational Semantics for While

DOI10.1007/978-3-642-03359-9_26MaRDI QIDQ3183540zbMATH OpenOpenAlexFDO

Authors Keiko Nakata, Tarmo Uustalu

Publication date 20 October 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-03359-9_26

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Recommendations

• A Hoare logic for the coinductive trace-based big-step semantics of While
• 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
• Coinductive big-step operational semantics
• Programming Languages and Systems

Cites work

• scientific article; zbMATH DE number 1223720 (Why is no real title available?)
• scientific article; zbMATH DE number 2085175 (Why is no real title available?)
• A note on Coinduction and Weak Bisimilarity for While Programs
• Abstract interpretation and application to logic programs
• An introduction to small scale reflection in Coq
• Bi-inductive structural semantics
• Coinductive big-step operational semantics
• Fractional Semantics
• General Recursion via Coinductive Types
• Generic Trace Semantics via Coinduction
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Transfinite semantics in the form of greatest fixpoint
• Typed Lambda Calculi and Applications

Cited in

(15)

• Coinductive big-step operational semantics
• Monads for behaviour
• A Hoare logic for the coinductive trace-based big-step semantics of While
• Compositional symbolic execution semantics
• Programming Languages and Systems
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• Denotational semantics for symbolic execution
• A Hoare logic for the coinductive trace-based big-step semantics of While
• Generalizing inference systems by coaxioms
• Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction
• A sequent calculus for trace formula implication
• A type system with subtyping for WebAssembly's stack polymorphism
• Bi-inductive structural semantics (extended abstract)
• Flag-based big-step semantics
• scientific article; zbMATH DE number 7037626 (Why is no real title available?)

Describes a project that uses

Uses Software

• CompCert
• Coq

This page was built for publication: Trace-Based Coinductive Operational Semantics for While

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3183540)