From operational semantics to abstract machines

DOI10.1017/S0960129500001559zbMath0798.68099OpenAlexW2104890704MaRDI QIDQ4279254

John Hannan, Dale A. Miller

Publication date: 31 October 1994

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129500001559

zbMATH Keywords

operational semanticsabstract machinesuntyped \(\lambda\)-calculuscorrectness of programming language implementationsintermediate-level specificationsmachine- verified correctness proofs

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)

Related Items (11)

A functional correspondence between call-by-need evaluators and lazy abstract machines ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Encoding transition systems in sequent calculus ⋮ Automating the functional correspondence between higher-order evaluators and abstract machines ⋮ A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation ⋮ State-transition machines, revisited ⋮ On Extracting Static Semantics ⋮ Formalizing Operational Semantic Specifications in Logic ⋮ A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation ⋮ Mechanized metatheory revisited ⋮ Rule-Based Operational Semantics for an Imperative Language

Cites Work

• Unnamed Item
• Unnamed Item
• The system \({\mathcal F}\) of variable types, fifteen years later
• Two-level semantics and code generation
• The categorical abstract machine
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Deriving Target Code as a Representation of Continuation Semantics
• The Mechanical Evaluation of Expressions
• A formulation of the simple theory of types

This page was built for publication: From operational semantics to abstract machines