The origins of structural operational semantics

DOI10.1016/j.jlap.2004.03.009zbMath1072.68063OpenAlexW2007809070MaRDI QIDQ1878710

Gordon D. Plotkin

Publication date: 8 September 2004

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2004.03.009

zbMATH Keywords

\(\lambda\)-calculusformal systems

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) History of computer science (68-03)

Related Items (54)

The Equational Theory of Weak Complete Simulation Semantics over BCCSP ⋮ From Outermost Reduction Semantics to Abstract Machine ⋮ Algebra Unifies Operational Calculi ⋮ Tiles for Reo ⋮ A Rewriting Logic Approach to Type Inference ⋮ Structural Operational Semantics for Weighted Transition Systems ⋮ A core calculus for correlation in orchestration languages ⋮ SOS formats and meta-theory: 20 years after ⋮ Splitting atoms safely ⋮ Processes with infinite liveness requirements ⋮ rCOS: Defining Meanings of Component-Based Software Architectures ⋮ Revisiting sequential composition in process calculi ⋮ Process calculi for biological processes ⋮ Programming language semantics: It’s easy as 1,2,3 ⋮ Measurable stochastics for Brane calculus ⋮ Better automata through process algebra ⋮ Equivalence checking 40 years after: a review of bisimulation tools ⋮ A semantic framework for proof evidence ⋮ iRho: an imperative rewriting calculus ⋮ Structural operational semantics through context-dependent behaviour ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Exploring conditional rewriting logic computations ⋮ Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming ⋮ Inspecting Rewriting Logic Computations (in a Parametric and Stepwise Way) ⋮ Notions of bisimulation and congruence formats for SOS with data ⋮ Hierarchical Design Rewriting with Maude ⋮ Inter-deriving semantic artifacts for object-oriented programming ⋮ A brief history of process algebra ⋮ CSP with Hierarchical State ⋮ Bisimulation and coinduction enhancements: a historical perspective ⋮ A Modular Equational Generalization Algorithm ⋮ Reactive Systems, Barbed Semantics, and the Mobile Ambients ⋮ Processes with local and global liveness requirements ⋮ Structural Operational Semantics with First-Order Logic ⋮ Automating Soundness Proofs ⋮ Bi-inductive structural semantics ⋮ The Rewriting Logic Semantics Project: A Progress Report ⋮ A Connector Algebra for P/T Nets Interactions ⋮ A Type System for Usage of Software Components ⋮ Probabilistic model of software approximate correctness ⋮ Dynamical Systems and Stochastic Programming: To Ordinary Differential Equations and Back ⋮ Algebra and logic for resource-based systems modelling ⋮ Formalizing Operational Semantic Specifications in Logic ⋮ Bio-PEPAd: a non-Markovian extension of Bio-PEPA ⋮ From Reduction-Based to Reduction-Free Normalization ⋮ Axiomatizing Weak Ready Simulation Semantics over BCCSP ⋮ A Theory Agenda for Component-Based Design ⋮ Syntactic Logical Relations for Polymorphic and Recursive Types ⋮ Bialgebraic Methods in Structural Operational Semantics ⋮ Bi-inductive Structural Semantics ⋮ A Congruence Rule Format with Universal Quantification ⋮ Compositional verification of asynchronous concurrent systems using CADP

Uses Software

• ALGOL 60

Cites Work

• Ten years of Hoare's logic: A survey. II: Nondeterminism
• On describing the behavior and implementation of distributed systems
• A calculus of communicating systems
• A mathematical semantics for a nondeterministic typed lambda-calculus
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• LCF considered as a programming language
• The Vienna development method: The meta-language
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• Countable nondeterminism and random assignment
• On the power of list iteration
• The Semantics of Call-By-Value and Call-By-Name in a Nondeterministic Environment
• Formal Semantics of Programming Languages: VDL
• Formal Justification of a Proof System for Communicating Sequential Processes
• A Model for Control Structures for Artificial Intelligence Programming Languages
• Formal verification of parallel programs
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Correspondence between ALGOL 60 and Church's Lambda-notation
• The next 700 programming languages
• Proving Properties of Programs by Structural Induction
• Random-Access Stored-Program Machines, an Approach to Programming Languages
• Monadic Elementary Formal Systems
• The Mechanical Evaluation of Expressions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The origins of structural operational semantics