Programming Language Semantics (Lectures Slides)

Category Theory......Page 1 Category......Page 3 Diagrams......Page 7 Cones & Limits......Page 10 Products......Page 16 Exponentials......Page 18 Lambda Calculus & Combinatory Logic......Page 21 Lambda Calculus (λ-Calculus)......Page 23 Syntax of λ-Calculus......Page 27 Free & Bound Variables......Page 29 Substitution......Page 31 α-Conversion......Page 35 β-Equivalence & β-Reduction......Page 37 Confluence of β-Reduction......Page 42 λ-Calculus as Programming Language......Page 45 Currying......Page 46 Church Booleans......Page 48 Pairs......Page 52 Church Numerals......Page 54 Adding Built-ins......Page 61 Recursion......Page 64 η-Equivalence......Page 73 Extensionality......Page 75 Combinatory Logic......Page 80 Simply Typed Lambda Calculus......Page 89 Syntax......Page 91 Terms......Page 92 Proof System......Page 95 Typing Algorithm......Page 98 Sets of Terms......Page 99 Equational Rules......Page 100 Models......Page 106 Full Type Frame......Page 111 Term Model......Page 114 Completeness......Page 121 Cartesian Closed Categories as Models for Simply-Typed λ-Calculus......Page 123 λ-Calculus captures Algebraic Specification......Page 128 (S, Σ)-CCC......Page 129 de Bruijn Nameless Representation of λ-Expression......Page 140 Extending Henkin Models......Page 143 Henkin Models are CCCs......Page 145 Some CCCs are Henkin Models......Page 146 Recursion......Page 148 Recursion in Term Rewriting......Page 150 Recursion in simple Imperative Languages......Page 158 Recursion in Higher Order Languages......Page 160 Recursion in Untyped λ-Calculus......Page 161 Mu Simply-Typed Lambda Calculus......Page 169 Programming Language for Computable Functions......Page 176 Transitional Semantics......Page 181 What about Completeness?......Page 190 Natural Semantics......Page 192 Complete Partial Orders......Page 195 Fixed-Point Theorem......Page 201 Fixed-Point Semantics of PCF......Page 206 Interpreting Types......Page 209 Interpreting Constants......Page 210 Interpreting Well-Typed Terms......Page 212 Polymorphism......Page 216 Types of Polymorphism......Page 217 Parametric/Universal Polymorphism......Page 219 Typing Rules......Page 222 Equational Rules......Page 223 Some Examples......Page 228 On Recursion......Page 232 More Examples......Page 234 Giving System F Executable Semantics......Page 242 Type Inference/Reconstruction......Page 243 Subtype Polymorphism......Page 245 Simply Typed λ-Calculus with Records......Page 246 Subtyping Rules......Page 249 Type System......Page 252 Equational Rules......Page 254 Subtyping & other Language Features......Page 256 Built-in Types......Page 257 Lists......Page 258 References......Page 259 Arrays......Page 265 Type Casting......Page 267 Syntax-directed Subtyping......Page 270 Typing Conditionals......Page 279 Subtypes & Objects......Page 284