Textbook
Programming Language FoundationsSeptember 2013, ©2014

Stump’s Programming Language Foundations is intended primarily for a graduatelevel course in programming languages theory which is standard in graduatelevel CS curricula. It may also be used in undergraduate programming theory courses but ONLY where students have a strong mathematical preparation.
Preface 1
I Central Topics 7
1 Semantics of FirstOrder Arithmetic 9
1.1 Syntax of FO(Z) terms 10
1.2 Informal semantics of FO(Z) terms 10
1.3 Syntax of FO(Z) formulas 11
1.4 Some alternative logical languages for arithmetic 12
1.5 Informal semantics of FO(Z) formulas 13
1.6 Formal semantics of FO(Z) terms 14
1.6.1 Examples 17
1.7 Formal semantics of FO(Z) formulas 18
1.7.1 Examples 18
1.8 Compositionality 19
1.9 Validity and satisfiability 19
1.10 Interlude: proof by naturalnumber induction 20
1.11 Proof by structural induction 27
1.12 Conclusion 28
1.13 Basic exercises 29
1.14 Intermediate exercises 30
2 Denotational Semantics of WHILE 33
2.1 Syntax and informal semantics of WHILE 33
2.2 Beginning of the formal semantics for WHILE 34
2.3 Problem with the semantics of whilecommands 35
2.4 Domains 37
2.5 Continuous functions 42
2.6 The least fixedpoint theorem 46
2.7 Completing the formal semantics of commands 48
2.8 Connection to practice: static analysis using abstract interpretation 54
2.9 Conclusion 59
2.10 Basic exercises 60
2.11 Intermediate exercises 62
3 Axiomatic Semantics of WHILE 65
3.1 Denotational equivalence 66
3.2 Partial correctness assertions 68
3.3 Interlude: rules and derivations 71
3.4 Hoare Logic rules 76
3.5 Example derivations in Hoare Logic 82
3.6 Soundness of Hoare Logic and induction on the structure of derivations 87
3.7 Conclusion 92
3.8 Exercises 92
4 Operational Semantics of WHILE 95
4.1 Bigstep semantics of WHILE 95
4.2 Smallstep semantics of WHILE 97
4.3 Relating the two operational semantics 101
4.4 Conclusion 120
4.5 Basic exercises 120
4.6 Intermediate exercises 122
5 Untyped Lambda Calculus 125
5.1 Abstract syntax of untyped lambda calculus 125
5.2 Operational semantics: full breduction 127
5.3 Defining full breduction with contexts 132
5.4 Specifying other reduction orders with contexts 134
5.5 Bigstep callbyvalue operational semantics 137
5.6 Relating bigstep and smallstep operational semantics 138
5.7 Conclusion 142
5.8 Basic Exercises 143
5.9 Intermediate Exercises 147
5.10 More Challenging Exercises 147
6 Programming in Untyped Lambda Calculus 149
6.1 The Church encoding for datatypes 149
6.2 The Scott encoding for datatypes 156
6.3 Other datatypes: lists 158
6.4 Nonrecursive operations on Scottencoded data 158
6.5 Recursive equations and the fix operator 160
6.6 Another recursive example: multiplication 162
6.7 Conclusion 162
6.8 Basic exercises 163
6.9 Intermediate exercises 164
7 Simple Type Theory 167
7.1 Abstract syntax of simple type theory 167
7.2 Semantics of types 168
7.3 Typeassignment rules 169
7.4 Semantic soundness for typeassignment rules 169
7.5 Applying semantic soundness to prove normalization 171
7.6 Type preservation 173
7.7 The CurryHoward isomorphism 176
7.8 Algorithmic typing 183
7.9 Algorithmic typing via constraint generation 186
7.10 Subtyping 190
7.11 Conclusion 199
7.12 Basic Exercises 200
7.13 Intermediate Exercises 202
II Extra Topics 205
8 Nondeterminism and Concurrency 207
8.1 Guarded commands 207
8.2 Operational semantics of guarded commands 208
8.3 Concurrent WHILE 215
8.4 Operational semantics of concurrent WHILE 216
8.5 Milner’s Calculus of Communicating Systems 219
8.6 Operational semantics of CCS 220
8.7 Conclusion 226
8.8 Basic exercises 226
8.9 Intermediate exercises 228
9 More on Untyped Lambda Calculus 231
9.1 Confluence of untyped lambda calculus 231
9.2 Combinators 259
9.3 Conclusion 266
9.4 Basic exercises 266
9.5 Intermediate exercises 267
10 Polymorphic Type Theory 269
10.1 Typeassignment version of System F 269
10.2 Annotated terms for System F 271
10.3 Semantics of annotated System F 272
10.4 Programming with Churchencoded data 274
10.5 Higherkind polymorphism and System Fw 276
10.6 Conclusion 283
10.7 Exercises 283
11 Functional Programming 285
11.1 Callbyvalue functional programming 286
11.2 Connection to practice: eager FP in OCaml
11.3 Lazy programming with callbyname evaluation 300
11.4 Connection to practice: lazy FP in Haskell 304
11.5 Conclusion 310
11.6 Basic Exercises 310
11.7 Intermediate exercises 312
Mathematical Background 315
Bibliography 321
Index 325
 Wiley ETexts are powered by VitalSource technologies ebook software.
 With Wiley ETexts you can access your ebook how and where you want to study: Online, Download and Mobile.
 Wiley etexts are nonreturnable and nonrefundable.
 WileyPLUS registration codes are NOT included with the Wiley EText. For informationon WileyPLUS, click here .
 To learn more about Wiley etexts, please refer to our FAQ.
 Ebooks are offered as ePubs or PDFs. To download and read them, users must install Adobe Digital Editions (ADE) on their PC.
 Ebooks have DRM protection on them, which means only the person who purchases and downloads the ebook can access it.
 Ebooks are nonreturnable and nonrefundable.
 To learn more about our ebooks, please refer to our FAQ.