Theories of programming languages

Table of contents

Preface
1 Predicate Logic
1.1 Abstract Syntax
1.2 Denotational Semantics of Predicate
Logic
1.3 Validity and Inference
1.4 Binding and Substitution
2 The Simple Imperative Language
2.1 Syntax
2.2 Denotational Semantics
2.3 Domains and Continuous Functions
2.4 The Least Fixed-Point Theorem
2.5 Variable Declarations and Substitution
2.6 Syntactic Sugar: The for Command
2.7 Arithmetic Errors
2.8 Soundness and Full Abstraction
3 Program Specifications and Their Proofs
3.1 Syntax and Semantics of Specifications
3.2 Inference Rules
3.3 Rules for Assignment and Sequential
Composition
3.4 Rules for while Commands
3.5 Further Rules
3.6 Computing Fibonacci Numbers
3.7 Fast Exponentiation
3.8 Complications and Limitations
4 Arrays
4.1 Abstract Syntax
4.2 Denotational Semantics
4.3 Binary Search
4.4 Inference Rules for Arrays
4.5 Higher-Order Assertions About Arrays
5 Failure, Input-Output, and Continuations
5.1 The fail Command
5.2 Intermediate Output and a Domain of Sequences
5.3 The Physical Argument for Continuity
5.4 Products and Disjoint Unions of Predomains
5.5 Recursive Domain Isomorphisms
5.6 Intermediate Input and a Domain of Resumptions
5.7 Continuation Semantics
5.8 Continuation Semantics of Extensions
6 Transition Semantics
6.1 Configurations and the Transition Relation
6.2 Inference Rules for the Simple Language
6.3 Transition Semantics of fail
6.4 Input and Output
7 Nondeterminism and Guarded Commands
7.1 Syntax and Transition Semantics
7.2 Bounded Nondeterminism and Powerdomains
7.3 Semantic Equations
7.4 Program Specification and Proof
7.5 Weakest Preconditions
8 Shared-Variable Concurrency
8.1 Concurrent Composition
8.2 Critical Regions
8.3 Mutual Exclusion and Conditional
Critical Regions
8.4 Deadlock
8.5 Fairness
8.6 Resumption Semantics
8.7 Transition Traces
8.8 Stuttering and Mumbling
9 Communicating Sequential Processes
9.1 Syntax
9.2 Transition Semantics
9.3 Possible Restrictions
9.4 Examples
9.5 Deadlock
9.6 Fairness
10 The Lambda Calculus
10.1 Syntax
10.2 Reduction
10.3 Normal-Order Evaluation
10.4 Eager Evaluation
10.5 Denotational Semantics
10.6 Programming in the Lambda Calculus
11 An Eager Functional Language
11.1 Concrete Syntax
11.2 Evaluation Semantics
11.3 Definitions, Patterns, and Recursion
11.4 Lists
11.5 Examples
11.6 Direct Denotational Semantics
11.7 Dynamic Binding
12 Continuations in a Functional Language
12.1 Continuation Semantics
12.2 Continuation as Values
12.3 Continuations as a Programming Technique
12.4 Deriving a First-Order Semantics
12.5 First-Order Semantics Summarized
12.6 Relating First-Order and Continuation Semantics
13 Iswim-like Languages
13.1 Aliasing, References, and States
13.2 Evaluation Semantics
13.3 Continuation Semantics
13.4 Some Syntactic Sugar
13.5 First-Order Semantics
13.6 Examples
13.7 Exceptions
13.8 Backtracking
13.9 Input and Output
13.10 Some Complications
14 A Normal-Order Language
14.1 Evaluation Semantics
14.2 Syntactic Sugar
14.3 Examples
14.4 Direct Denotational Semantics
14.5 Reduction Revisited
14.6 Lazy Evaluation
15 The Simple Type System
15.1 Types, Contexts, and Judgements
15.2 Inference Rules
15.3 Explicit Typing
15.4 The Extrinsic Meaning of Types
15.5 The Intrinsic View
15.6 Set-Theoretic Semantics
15.7 Recursive Types
16 Subtypes and Intersection Types
16.1 Inference Rules for Subtyping
16.2 Named Products and Sums
16.3 Intersection Types
16.4 Extrinsic Semantics
16.5 Generic Operators
16.6 Intrinsic Semantics
17 Polymorphism
17.1 Syntax and Inference Rules
17.2 Polymorphic Programming
17.3 Extrinsic Semantics
18 Module Specification
18.1 Type Definitions
18.2 Existential Quantification and Modules
18.3 Implementing One Abstraction in Terms of Another
19 Algo-like Languages
19.1 Data Types and Phrase Types
19.2 Phrases and Type Inference Rules
19.3 Examples
19.4 Arrays and Declarators
19.5 A Semantics Embodying the Stack
Discipline
19.6 The Semantics of Variables
19.7 The Semantics of Procedures
19.8 Some Extensions and Simplifications
Appendix: Mathematical Background
A.1 Sets
A.2 Relations
A.3 Functions
A.4 Relations and Functions Between Sets
A.5 More About Products and Disjoint Unions
A.6 More About Relations
Bibliography
Index