Formalizing Operational Semantic Specifications in Logic

DOI10.1016/j.entcs.2009.07.020zbMath1347.68213OpenAlexW1996070941MaRDI QIDQ4982629

Dale A. Miller

Publication date: 9 April 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.07.020

zbMATH Keywords

operational semanticsspecificationsmultiset rewritingbig-step SOS semanticssmall-step SOS semantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Uses Software

• ML
• Twelf
• Bedwyr
• PoplMark
• Lolli

Cites Work

• Forum: A multiple-conclusion specification logic
• A calculus of communicating systems
• The chemical abstract machine
• A calculus of mobile processes. II
• Logic programming in a fragment of intuitionistic linear logic
• The origins of structural operational semantics
• A structural approach to operational semantics
• Petri nets, Horn programs, linear logic and vector games
• Uniform proofs as a foundation for logic programming
• From operational semantics to abstract machines
• A proof theory for generic judgments
• Theorem Proving in Higher Order Logics
• The Mechanical Evaluation of Expressions
• Sequential abstract-state machines capture sequential algorithms
• Reasoning with higher-order abstract syntax in a logical framework
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item