Computation and Deduction
Frank Pfenning · 2020
Syntax : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7 2.2 Substitution : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 10 2.3 Operational Semantics : : : : : : : : : : : : : : : : : : : : : : : : : : 11 2.4 A First Meta-Theorem: Evaluation Returns a Value : : : : : : : : : 15 2.5 The Type System : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 18 2.6 Type Preservation : : : : : : : : : : : : : : : : : : : : : : : : : : : : 21 2.7 Further Discussion : : : : : : : : : : : : : : : : : : : : : : : : : : : : 25 2.8 Exercises : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 28 3 Formalization in a Logical Framework 33 3.1 The Simply-Typed Fragment of LF : : : : : : : : : : : : : : : : : : : 34 3.2 Higher-Order Abstract Syntax : : : : : : : : : : : : : : : : : : : : : 36 3.3 Representing Mini-ML Expressions : : : : : : : : : : : : : : : : : : : 41 3.4 Judgments as Types : : : : : : : : : : : : : : : : : : : : : : : : : : : 46 3.5 Adding...