Lecture Notes on Denotational Semantics

Contents......Page 2
Preface......Page 4
1 Introduction......Page 5
Basic example of denotational semantics......Page 6
Example - while-loops as fixed points......Page 11
Exercises......Page 16
Posets & monotone functions......Page 17
Least elements & pre-fixed points......Page 20
CPOs & continuous functions......Page 23
Tarski fixed point theorem......Page 33
Exercises......Page 35
Flat domains......Page 36
Products of domains......Page 37
Function domains......Page 41
Exercises......Page 45
Chain-closed & admissible subsets......Page 47
Examples......Page 48
Building chain-closed subsets......Page 50
Exercises......Page 53
Terms & types......Page 54
Free variables, bound variables & substitution......Page 55
Typing......Page 56
Evaluation......Page 59
Contextual equivalence......Page 63
Denotational semantics......Page 65
Exercises......Page 67
Denotation of types......Page 69
Denotation of terms......Page 70
Compositionality......Page 77
Soundness......Page 79
Exercises......Page 80
Formal approximation relations......Page 81
Proof of the Fundamental Property of......Page 84
Extensionality......Page 87
Exercises......Page 90
Failure of full abstraction......Page 91
PCF+por......Page 97
Fully abstract semantics for PCF......Page 98
Exercises......Page 99
Refs......Page 100
Errata......Page 102