abstract-machine - SKILL.md Agent Skill

name: abstract-machine description: "Implement abstract machines for defining and executing operational semantics of programming languages." version: "1.0.0" tags: [semantics, interpreters, popl, theory] difficulty: intermediate languages: [haskell, ocaml, python] dependencies: [lambda-calculus-interpreter, operational-semantics-definer]

Abstract Machine

Abstract machines define operational semantics by specifying computation as transitions between configurations. They bridge formal semantics and practical interpreters, enabling both reasoning about programs and efficient implementation.

When to Use This Skill

Defining operational semantics for languages
Building efficient interpreters
Reasoning about program evaluation
Implementing virtual machines
Teaching programming language theory

What This Skill Does

Configuration Definition: Define machine state (code, environment, continuation)
Transition Rules: Specify how configurations evolve
Stack Management: Handle control flow with continuations
Environment Handling: Manage variable bindings
Termination Detection: Identify final states

Key Concepts

Concept	Description
Configuration	Complete machine state at a point
Control	Expression or value being processed
Environment	Variable bindings
Continuation	What to do next (stack)
Transition	Rule for moving between configurations

Tips

Use de Bruijn indices to avoid variable capture
CEK is good for call-by-value
Krivine is elegant for call-by-name
SECD was designed for functional languages
Defunctionalize continuations for compilers

Common Use Cases

Formalizing language semantics
Building interpreters
Proving type safety
Implementing virtual machines
Teaching PL concepts

Related Skills

lambda-calculus-interpreter - Direct style interpretation
operational-semantics-definer - Small-step/big-step semantics
denotational-semantics-builder - Mathematical semantics
cps-transformer - Continuation-passing style

Canonical References

Reference	Why It Matters
Felleisen & Friedman, "Control Operators, the SECD-Machine, and the λ-Calculus" (1986)	CEK machine
Landin, "The Mechanical Evaluation of Expressions" (1964)	SECD machine
Krivine, "A Call-by-Name Lambda-Calculus Machine" (published 2007, developed earlier)	Krivine machine

Tradeoffs and Limitations

Approach Tradeoffs

Approach	Pros	Cons
CEK	Simple, CBN/CBV variants	Explicit environments
SECD	Stack-based, familiar	More complex state
Krivine	Elegant for CBN	Not for CBV

When NOT to Use This Skill

When denotational semantics is more appropriate
For simple expression evaluation
When efficiency is the only concern

Limitations

May be less intuitive than big-step
Need to handle errors explicitly
Control flow can be spread across rules

Assessment Criteria

A high-quality implementation should have:

Criterion	What to Look For
Completeness	Handles all language constructs
Determinism	Each configuration has unique successor
Termination	Reaches final state for terminating programs
Correctness	Matches expected semantics

Quality Indicators

✅ Good: Complete transition rules, handles all cases, matches expected semantics ⚠️ Warning: Missing some constructs, stuck states ❌ Bad: Non-deterministic, doesn't terminate correctly

Research Tools & Artifacts

Real-world abstract machine implementations to study:

Artifact	Why It Matters
GHC's STG machine	Production call-by-need machine with sparks, blackholes, info tables
Lua 5.3 VM	Simple, efficient register-based VM with upvalues and coroutines
JavaScript V8 Ignition	Register-based bytecode interpreter with turbofan integration
OCaml bytecode interpreter	Direct-style VM with closures and effect handlers
JVM HotSpot interpreter	Stack-based with JIT compilation hints
WebAssembly reference interpreter	Formal specification machine

Key Implementations to Study

PyPy interpreter (RPython): How meta-tracing works with the VM
LuaJIT: Efficient closure representation and JIT compilation
GHCi interpreter: Bytecode-based REPL for Haskell

Research Frontiers

Current active research in abstract machines:

Direction	Key Papers	Challenge
Effect handlers	"Handlers of Algebraic Effects" (Plotkin & Pretnar, 2009)	Encoding algebraic effects in CEK/Krivine
Delimited continuations	"Control Delimiters and their Hierarchies" (Felleisen, 1988)	Multiple prompts, composable snapshots
Multi-stage	"MetaOCaml" (2003)	Staging the machine itself
WebAssembly	"A Formal Specification" (2020)	Verification of the reference interpreter
Zero-cost exceptions	"Zero-cost Exception Handling" (2018)	Efficient error paths without overhead

Hot Topics

Compacting collectors for VM heaps: GCs designed for short-lived bytecode
Speculative optimization: Profile-guided specialization at runtime
Hardware-enforced isolation: CHERI capabilities in VM design

Implementation Pitfalls

Common bugs in production abstract machine implementations:

Pitfall	Real Example	Prevention
Stack overflow	Early OCaml bytecode had limited stack	Grow stacks dynamically, detect overflow
Space leaks	GHC's CAF retention issues	Analyze closure usage, prune unused
Wrong tail recursion	Early JavaScript engines	Verify tail call optimization (TCO)
Closure escape	Lua's upvalue capture bugs	Track closure lifetimes precisely
Wrong environment capture	Python's late binding closures	Capture by value vs reference
Improper frame pointers	Debug builds vs optimized	Preserve stack frame invariants

The "Space Leak" Story

GHC once had a famous space leak where CAFs (Constant Applicative Forms) retained heap:

-- This creates a CAF that retains xs
result = map expensiveFunction veryLargeList
-- Forces entire list despite laziness

Solution: Selective CAF elimination, scrutinize, and blackholes for synchronization.

Tail Call Optimization Pitfalls

Wrong TCO can cause crashes:

Must check accumulator patterns correctly
Must handle mutual recursion
Must preserve tail position across branches
Debugging: stack traces differ in tail-recursive code