| Preface | ix |
| 1 | Predicate Logic | 1 |
|---|
| 1.1 | Abstract Syntax | 1 |
| 1.2 | Denotational Semantics of Predicate Logic | 8 |
| 1.3 | Validity and Inference | 12 |
| 1.4 | Binding and Substitution | 15 |
| 2 | The Simple Imperative Language | 24 |
|---|
| 2.1 | Syntax | 24 |
| 2.2 | Denotational Semantics | 26 |
| 2.3 | Domains and Continuous Functions | 29 |
| 2.4 | The Least Fixed-Point Theorem | 35 |
| 2.5 | Variable Declarations and Substitution | 39 |
| 2.6 | Syntactic Sugar: The for Command | 45 |
| 2.7 | Arithmetic Errors | 47 |
| 2.8 | Soundness and Full Abstraction | 48 |
| 3 | Program Specifications and Their Proofs | 54 |
|---|
| 3.1 | Syntax and Semantics of Specifications | 55 |
| 3.2 | Inference Rules | 57 |
| 3.3 | Rules for Assignment and Sequential Composition | 57 |
| 3.4 | Rules for while Commands | 63 |
| 3.5 | Further Rules | 66 |
| 3.6 | Computing Fibonacci Numbers | 69 |
| 3.7 | Fast Exponentiation | 71 |
| 3.8 | Complications and Limitations | 74 |
| 4 | Arrays | 81 |
|---|
| 4.1 | Abstract Syntax | 81 |
| 4.2 | Denotational Semantics | 83 |
| 4.3 | Binary Search | 85 |
| 4.4 | Inference Rules for Arrays | 90 |
| 4.5 | Higher-Order Assertions About Arrays | 93 |
| 5 | Failure, Input-Output, and Continuations | 97 |
|---|
| 5.1 | The fail Command | 97 |
| 5.2 | Intermediate Output and a Domain of Sequences | 101 |
| 5.3 | The Physical Argument for Continuity | 107 |
| 5.4 | Products and Disjoint Unions of Predomains | 109 |
| 5.5 | Recursive Domain Isomorphisms | 111 |
| 5.6 | Intermediate Input and a Domain of Resumptions | 113 |
| 5.7 | Continuation Semantics | 115 |
| 5.8 | Continuation Semantics of Extensions | 118 |
| 6 | Transition Semantics | 126 |
|---|
| 6.1 | Configurations and the Transition Relation | 126 |
| 6.2 | Inference Rules for the Simple Language | 127 |
| 6.3 | Transition Semantics of fail | 131 |
| 6.4 | Input and Output | 132 |
| 7 | Nondeterminism and Guarded Commands | 136 |
|---|
| 7.1 | Syntax and Transition Semantics | 137 |
| 7.2 | Bounded Nondeterminism and Powerdomains | 139 |
| 7.3 | Semantic Equations | 144 |
| 7.4 | Program Specification and Proof | 147 |
| 7.5 | Weakest Preconditions | 149 |
| 8 | Shared-Variable Concurrency | 155 |
|---|
| 8.1 | Concurrent Composition | 155 |
| 8.2 | Critical Regions | 157 |
| 8.3 | Mutual Exclusion and Conditional Critical Regions | 159 |
| 8.4 | Deadlock | 161 |
| 8.5 | Fairness | 162 |
| 8.6 | Resumption Semantics | 164 |
| 8.7 | Transition Traces | 165 |
| 8.8 | Stuttering and Mumbling | 171 |
| 9 | Communicating Sequential Processes | 181 |
|---|
| 9.1 | Syntax | 181 |
| 9.2 | Transition Semantics | 183 |
| 9.3 | Possible Restrictions | 187 |
| 9.4 | Examples | 188 |
| 9.5 | Deadlock | 189 |
| 9.6 | Fairness | 189 |
| 10 | The Lambda Calculus | 194 |
|---|
| 10.1 | Syntax | 196 |
| 10.2 | Reduction | 197 |
| 10.3 | Normal-Order Evaluation | 201 |
| 10.4 | Eager Evaluation | 206 |
| 10.5 | Denotational Semantics | 208 |
| 10.6 | Programming in the Lambda Calculus | 216 |
| 11 | An Eager Functional Language | 222 |
|---|
| 11.1 | Concrete Syntax | 222 |
| 11.2 | Evaluation Semantics | 223 |
| 11.3 | Definitions, Patterns, and Recursion | 228 |
| 11.4 | Lists | 231 |
| 11.5 | Examples | 232 |
| 11.6 | Direct Denotational Semantics | 235 |
| 11.7 | Dynamic Binding | 242 |
| 12 | Continuations in a Functional Language | 251 |
|---|
| 12.1 | Continuation Semantics | 251 |
| 12.2 | Continuations as Values | 255 |
| 12.3 | Continuations as a Programming Technique | 257 |
| 12.4 | Deriving a First-Order Semantics | 258 |
| 12.5 | First-Order Semantics Summarized | 264 |
| 12.6 | Relating First-Order and Continuation Semantics | 269 |
| 13 | Iswim-like Languages | 273 |
|---|
| 13.1 | Aliasing, References, and States | 273 |
| 13.2 | Evaluation Semantics | 276 |
| 13.3 | Continuation Semantics | 278 |
| 13.4 | Some Syntactic Sugar | 282 |
| 13.5 | First-Order Semantics | 282 |
| 13.6 | Examples | 284 |
| 13.7 | Exceptions | 287 |
| 13.8 | Backtracking | 289 |
| 13.9 | Input and Output | 291 |
| 13.10 | Some Complications | 293 |
| 14 | A Normal-Order Language | 298 |
|---|
| 14.1 | Evaluation Semantics | 298 |
| 14.2 | Syntactic Sugar | 301 |
| 14.3 | Examples | 302 |
| 14.4 | Direct Denotational Semantics | 304 |
| 14.5 | Reduction Revisited | 306 |
| 14.6 | Lazy Evaluation | 307 |
| 15 | The Simple Type System | 315 |
|---|
| 15.1 | Types, Contexts, and Judgements | 316 |
| 15.2 | Inference Rules | 318 |
| 15.3 | Explicit Typing | 324 |
| 15.4 | The Extrinsic Meaning of Types | 327 |
| 15.5 | The Intrinsic View | 334 |
| 15.6 | Set-Theoretic Semantics | 339 |
| 15.7 | Recursive Types | 341 |
| 16 | Subtypes and Intersection Types | 349 |
|---|
| 16.1 | Inference Rules for Subtyping | 349 |
| 16.2 | Named Products and Sums | 352 |
| 16.3 | Intersection Types | 354 |
| 16.4 | Extrinsic Semantics | 358 |
| 16.5 | Generic Operators | 362 |
| 16.6 | Intrinsic Semantics | 365 |
| 17 | Polymorphism | 379 |
|---|
| 17.1 | Syntax and Inference Rules | 380 |
| 17.2 | Polymorphic Programming | 383 |
| 17.3 | Extrinsic Semantics | 390 |
| 18 | Module Specification | 398 |
|---|
| 18.1 | Type Definitions | 398 |
| 18.2 | Existential Quantification and Modules | 401 |
| 18.3 | Implementing One Abstraction in Terms of Another | 406 |
| 19 | Algol-like Languages | 415 |
|---|
| 19.1 | Data Types and Phrase Types | 416 |
| 19.2 | Phrases and Type Inference Rules | 419 |
| 19.3 | Examples | 423 |
| 19.4 | Arrays and Declarators | 426 |
| 19.5 | A Semantics Embodying the Stack Discipline | 428 |
| 19.6 | The Semantics of Variables | 434 |
| 19.7 | The Semantics of Procedures | 436 |
| 19.8 | Some Extensions and Simplifications | 439 |
| Appendix: Mathematical Background | 447 |
|---|
| A.1 | Sets | 448 |
| A.2 | Relations | 450 |
| A.3 | Functions | 452 |
| A.4 | Relations and Functions Between Sets | 456 |
| A.5 | More About Products and Disjoint Unions | 459 |
| A.6 | More About Relations | 462 |
| Bibliography | 467 |
| Index | 483 |