Extrinsically Typed Operational Semantics for Functional Languages
summary
Lang-n-check automates checking of language specifications by taking an extrinsically typed operational semantics and verifying that typing rules and reduction rules align to yield type soundness proofs or concrete counterexamples. The tool reads language syntax and rule files, performs syntactic and semantic checks, and either emits machine-checkable evidence of preservation and progress or pinpoints offending rules. The demo focuses on functional-language fragments and reports whether the specification passes the soundness checks.
AI-written summary · about
chapters (9)
- 0:00Intro
- 1:06How do we use types in PL?
- 1:35Can we apply this approach to type checking languages?
- 3:22What Language Definitions?
- 5:30Can we classify the operators of the language?
- 8:34Are Operations Well-Defined?
- 10:04Are Evaluation Contexts Well-Defined?
- 11:44Lang-n-check
- 14:43Informative Error Messages
related talks
40mFormal semantics for multi-language programs- 40mFormal semantics for multi-language programs
31mProgramming Languages Must Have Formal Semantics. Period.
46mThe Calculated Typer (Functional Pearl)
02h 50mIntro to Type Systems and Operational Semantics
53mSemantics-based program manipulation in the age of LLMs
01h 05mAll the Languages Together
19mA Pure Demand Operational Semantics with Applications to Program Analysis