Theories of Programming Languages (John C. Reynolds)

Table of Contents

Prefaceix
1Predicate Logic1
1.1Abstract Syntax1
1.2Denotational Semantics of Predicate Logic8
1.3Validity and Inference12
1.4Binding and Substitution15
2The Simple Imperative Language24
2.1Syntax24
2.2Denotational Semantics26
2.3Domains and Continuous Functions29
2.4The Least Fixed-Point Theorem35
2.5Variable Declarations and Substitution39
2.6Syntactic Sugar: The for Command45
2.7Arithmetic Errors47
2.8Soundness and Full Abstraction48
3Program Specifications and Their Proofs54
3.1Syntax and Semantics of Specifications55
3.2Inference Rules57
3.3Rules for Assignment and Sequential Composition57
3.4Rules for while Commands63
3.5Further Rules66
3.6Computing Fibonacci Numbers69
3.7Fast Exponentiation71
3.8Complications and Limitations74
4Arrays81
4.1Abstract Syntax81
4.2Denotational Semantics83
4.3Binary Search85
4.4Inference Rules for Arrays90
4.5Higher-Order Assertions About Arrays93
5Failure, Input-Output, and Continuations97
5.1The fail Command97
5.2Intermediate Output and a Domain of Sequences101
5.3The Physical Argument for Continuity107
5.4Products and Disjoint Unions of Predomains109
5.5Recursive Domain Isomorphisms111
5.6Intermediate Input and a Domain of Resumptions113
5.7Continuation Semantics115
5.8Continuation Semantics of Extensions118
6Transition Semantics126
6.1Configurations and the Transition Relation126
6.2Inference Rules for the Simple Language127
6.3Transition Semantics of fail131
6.4Input and Output132
7Nondeterminism and Guarded Commands136
7.1Syntax and Transition Semantics137
7.2Bounded Nondeterminism and Powerdomains139
7.3Semantic Equations144
7.4Program Specification and Proof147
7.5Weakest Preconditions149
8Shared-Variable Concurrency155
8.1Concurrent Composition155
8.2Critical Regions157
8.3Mutual Exclusion and Conditional Critical Regions159
8.4Deadlock161
8.5Fairness162
8.6Resumption Semantics164
8.7Transition Traces165
8.8Stuttering and Mumbling171
9Communicating Sequential Processes181
9.1Syntax181
9.2Transition Semantics183
9.3Possible Restrictions187
9.4Examples188
9.5Deadlock189
9.6Fairness189
10The Lambda Calculus194
10.1Syntax196
10.2Reduction197
10.3Normal-Order Evaluation201
10.4Eager Evaluation206
10.5Denotational Semantics208
10.6Programming in the Lambda Calculus216
11An Eager Functional Language222
11.1Concrete Syntax222
11.2Evaluation Semantics223
11.3Definitions, Patterns, and Recursion228
11.4Lists231
11.5Examples232
11.6Direct Denotational Semantics235
11.7Dynamic Binding242
12Continuations in a Functional Language251
12.1Continuation Semantics251
12.2Continuations as Values255
12.3Continuations as a Programming Technique257
12.4Deriving a First-Order Semantics258
12.5First-Order Semantics Summarized264
12.6Relating First-Order and Continuation Semantics269
13Iswim-like Languages273
13.1Aliasing, References, and States273
13.2Evaluation Semantics276
13.3Continuation Semantics278
13.4Some Syntactic Sugar282
13.5First-Order Semantics282
13.6Examples284
13.7Exceptions287
13.8Backtracking289
13.9Input and Output291
13.10Some Complications293
14A Normal-Order Language298
14.1Evaluation Semantics298
14.2Syntactic Sugar301
14.3Examples302
14.4Direct Denotational Semantics304
14.5Reduction Revisited306
14.6Lazy Evaluation307
15The Simple Type System315
15.1Types, Contexts, and Judgements316
15.2Inference Rules318
15.3Explicit Typing324
15.4The Extrinsic Meaning of Types327
15.5The Intrinsic View334
15.6Set-Theoretic Semantics339
15.7Recursive Types341
16Subtypes and Intersection Types349
16.1Inference Rules for Subtyping349
16.2Named Products and Sums352
16.3Intersection Types354
16.4Extrinsic Semantics358
16.5Generic Operators362
16.6Intrinsic Semantics365
17Polymorphism379
17.1Syntax and Inference Rules380
17.2Polymorphic Programming383
17.3Extrinsic Semantics390
18Module Specification398
18.1Type Definitions398
18.2Existential Quantification and Modules401
18.3Implementing One Abstraction in Terms of Another406
19Algol-like Languages415
19.1Data Types and Phrase Types416
19.2Phrases and Type Inference Rules419
19.3Examples423
19.4Arrays and Declarators426
19.5A Semantics Embodying the Stack Discipline428
19.6The Semantics of Variables434
19.7The Semantics of Procedures436
19.8Some Extensions and Simplifications439
Appendix: Mathematical Background447
A.1Sets448
A.2Relations450
A.3Functions452
A.4Relations and Functions Between Sets456
A.5More About Products and Disjoint Unions459
A.6More About Relations462
Bibliography467
Index483
John.Reynolds@cs.cmu.edu (home page)
last updated February 7, 1999