操作語意 / Operational Semantics
- Introduction to semantics of functional programming
Outline
-
- Syntax and typing rules for PCF
- Small-step and big-step semantics
- Type safety
-
- Correctness
- Computational adequacy
- Compactness
- Fixed point induction
-
- Formalising syntax and typing rules
- Extracting an interpreter of PCF
Reference
- Robert Harper. Practical Foundations for Programming Languages. Cambridge University Press, 2012.
- Thomas Streicher. Domain-Theoretic Foundations of Functional Programming. World Scientific, 2006
- Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.
