Shared flowchart

Software · L5 · Semantics Styles and Type Soundness

Sign in to clone

How operational and denotational semantics relate, and how Progress plus Preservation combine into type soundness.

by @openstemUpdated Software
Program syntax eOperational semanticsDenotational semantics: compositional map into a domainSmall-step: e -> e' (one reduction at a time)Big-step: e ⇓ v (final value in one judgement)Stuck term: not a value, no rule applies (the bug type soundness rules out)CPO domain + least fixed point (Kleene) models recursion/loopsType system Γ ⊢ e : τProgress: well-typed e is a value or can stepPreservation: e -> e' preserves the type τType soundness: well-typed programs never get stuck

We use privacy-friendly product analytics (no session recording, PII masked) to improve OpenStem. Load analytics? Privacy Policy