Trace-Based Coinductive Operational Semantics for While

DOI10.1007/978-3-642-03359-9_26zbMath1252.68056OpenAlexW1585398629MaRDI QIDQ3183540

Tarmo Uustalu, Keiko Nakata

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)

Related Items

Monads for behaviour ⋮ A type system with subtyping for WebAssembly's stack polymorphism ⋮ Generalizing Inference Systems by Coaxioms ⋮ Characteristic formulae for liveness properties of non-terminating CakeML programs ⋮ Flag-based big-step semantics ⋮ Unnamed Item

Uses Software

• Coq
• CompCert

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• Bi-inductive structural semantics
• Coinductive big-step operational semantics
• Fractional Semantics
• Abstract interpretation and application to logic programs
• A note on Coinduction and Weak Bisimilarity for While Programs
• General Recursion via Coinductive Types
• Generic Trace Semantics via Coinduction
• Typed Lambda Calculi and Applications

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