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

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

• 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
• Unnamed Item
• Unnamed Item

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