Logical specification of operational semantics

DOI10.1007/3-540-48168-0_4MaRDI QIDQ4945216zbMATH OpenFDO

Authors Peter D. Mosses

Publication date 7 October 2001

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

Full work available at URL https://doi.org/10.1007/3-540-48168-0_4

zbMATH Keywords

operational semantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Review text

The relationship between various logic-based frameworks for specifying the operational semantics of programming languages and concurrent systems is surveyed. Considered logics for inferring judgments about program executions include arbitrary inference systems, natural deduction systems, Horn logic, equational logic, rewriting logic and tile logic. The author points out relationships between these applied logics, their merits and drawbacks. This survey is a good introduction to the main techniques for logical specification of operational semantics. For the entire collection see [Zbl 0929.00039].

Recommendations

• Formalizing operational semantic specifications in logic
• Representing and Reasoning with Operational Semantics
• A rewriting logic approach to operational semantics
• Programming Languages and Systems
• scientific article; zbMATH DE number 936829

Cited in

(9)

• Operational semantics and generalized weakest preconditions
• Formal foundations of operational semantics
• Rewriting logic: Roadmap and bibliography
• Modular structural operational semantics
• Rule-based operational semantics for an imperative language
• Representing and Reasoning with Operational Semantics
• scientific article; zbMATH DE number 1231615 (Why is no real title available?)
• Formalizing operational semantic specifications in logic
• scientific article; zbMATH DE number 6787693 (Why is no real title available?)

This page was built for publication: Logical specification of operational semantics

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