Theories of Programming Languages

Cover......Page 1
Title......Page 4
Copyright......Page 5
Contents......Page 6
Preface......Page 10
1.1 Abstract Syntax......Page 14
1.2 Denotational Semantics of Predicate Logic......Page 21
1.3 Validity and Inference......Page 25
1.4 Binding and Substitution......Page 28
2.1 Syntax......Page 37
2.2 Denotational Semantics......Page 39
2.3 Domains and Continuous Functions......Page 42
2.4 The Least Fixed-Point Theorem......Page 48
2.5 Variable Declarations and Substitution......Page 52
2.6 Syntactic Sugar: The for Command......Page 58
2.7 Arithmetic Errors......Page 60
2.8 Soundness and Full Abstraction......Page 61
3 Program Specifications and Their Proofs......Page 67
3.1 Syntax and Semantics of Specifications......Page 68
3.3 Rules for Assignment and Sequential Composition......Page 70
3.4 Rules for while Commands......Page 76
3.5 Further Rules......Page 79
3.6 Computing Fibonacci Numbers......Page 82
3.7 Fast Exponentiation......Page 84
3.8 Complications and Limitations......Page 87
4.1 Abstract Syntax......Page 94
4.2 Denotational Semantics......Page 96
4.3 Binary Search......Page 98
4.4 Inference Rules for Arrays......Page 103
4.5 Higher-Order Assertions About Arrays......Page 106
5.1 The fail Command......Page 110
5.2 Intermediate Output and a Domain of Sequences......Page 114
5.3 The Physical Argument for Continuity......Page 120
5.4 Products and Disjoint Unions of Predomains......Page 122
5.5 Recursive Domain Isomorphisms......Page 124
5.6 Intermediate Input and a Domain of Resumptions......Page 126
5.7 Continuation Semantics......Page 128
5.8 Continuation Semantics of Extensions......Page 131
6.1 Configurations and the Transition Relation......Page 139
6.2 Inference Rules for the Simple Language......Page 140
6.3 Transition Semantics of fail......Page 144
6.4 Input and Output......Page 145
7 Nondeterminism and Guarded Commands......Page 149
7.1 Syntax and Transition Semantics......Page 150
7.2 Bounded Nondeterminism and Powerdomains......Page 152
7.3 Semantic Equations......Page 157
7.4 Program Specification and Proof......Page 160
7.5 Weakest Preconditions......Page 162
8.1 Concurrent Composition......Page 168
8.2 Critical Regions......Page 170
8.3 Mutual Exclusion and Conditional Critical Regions......Page 172
8.4 Deadlock......Page 174
8.5 Fairness......Page 175
8.6 Resumption Semantics......Page 177
8.7 Transition Traces......Page 178
8.8 Stuttering and Mumbling......Page 184
9.1 Syntax......Page 194
9.2 Transition Semantics......Page 196
9.3 Possible Restrictions......Page 200
9.4 Examples......Page 201
9.6 Fairness......Page 202
10 The Lambda Calculus......Page 207
10.1 Syntax......Page 209
10.2 Reduction......Page 210
10.3 Normal-Order Evaluation......Page 214
10.4 Eager Evaluation......Page 219
10.5 Denotational Semantics......Page 221
10.6 Programming in the Lambda Calculus......Page 229
11.1 Concrete Syntax......Page 235
11.2 Evaluation Semantics......Page 236
11.3 Definitions, Patterns, and Recursion......Page 241
11.4 Lists......Page 244
11.5 Examples......Page 245
11.6 Direct Denotational Semantics......Page 248
11.7 Dynamic Binding......Page 255
12.1 Continuation Semantics......Page 264
12.2 Continuations as Values......Page 268
12.3 Continuations as a Programming Technique......Page 270
12.4 Deriving a First-Order Semantics......Page 271
12.5 First-Order Semantics Summarized......Page 277
12.6 Relating First-Order and Continuation Semantics......Page 282
13.1 Aliasing, References, and States......Page 286
13.2 Evaluation Semantics......Page 289
13.3 Continuation Semantics......Page 291
13.5 First-Order Semantics......Page 295
13.6 Examples......Page 297
13.7 Exceptions......Page 300
13.8 Backtracking......Page 302
13.9 Input and Output......Page 304
13.10 Some Complications......Page 306
14.1 Evaluation Semantics......Page 311
14.2 Syntactic Sugar......Page 314
14.3 Examples......Page 315
14.4 Direct Denotational Semantics......Page 317
14.5 Reduction Revisited......Page 319
14.6 Lazy Evaluation......Page 320
15 The Simple Type System......Page 328
15.1 Types, Contexts, and Judgements......Page 329
15.2 Inference Rules......Page 331
15.3 Explicit Typing......Page 337
15.4 The Extrinsic Meaning of Types......Page 340
15.5 The Intrinsic View......Page 347
15.6 Set-Theoretic Semantics......Page 352
15.7 Recursive Types......Page 354
16.1 Inference Rules for Subtyping......Page 362
16.2 Named Products and Sums......Page 365
16.3 Intersection Types......Page 367
16.4 Extrinsic Semantics......Page 371
16.5 Generic Operators......Page 375
16.6 Intrinsic Semantics......Page 378
17 Polymorphism......Page 392
17.1 Syntax and Inference Rules......Page 393
17.2 Polymorphic Programming......Page 396
17.3 Extrinsic Semantics......Page 403
18.1 Type Definitions......Page 411
18.2 Existential Quantification and Modules......Page 414
18.3 Implementing One Abstraction in Terms of Another......Page 419
19 Algol-like Languages......Page 428
19.1 Data Types and Phrase Types......Page 429
19.2 Phrases and Type Inference Rules......Page 432
19.3 Examples......Page 436
19.4 Arrays and Declarators......Page 439
19.5 A Semantics Embodying the Stack Discipline......Page 441
19.6 The Semantics of Variables......Page 447
19.7 The Semantics of Procedures......Page 449
19.8 Some Extensions and Simplifications......Page 452
Appendix: Mathematical Background......Page 460
A.1 Sets......Page 461
A.2 Relations......Page 463
A.3 Functions......Page 465
A.4 Relations and Functions Between Sets......Page 469
A.5 More About Products and Disjoint Unions......Page 472
A.6 More About Relations......Page 475
Bibliography......Page 480
Index......Page 496