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