Contents
Part I Control structures for imperative languages
Chapter 1 Early programming languages
1.1 Control flow in processors
1.2 Machine languages, assembly languages
1.3 FORTRAN
1.4 ALGOL 60
1.5 Conditionals and loops
1.6 Early exit from loops and blocks
1.7 Further reading
Chapter 2 Structured programming
2.1 A movement and a controversy
2.2 Programming without goto
2.3 Expressiveness of structured programming
2.4 Reductions between control structures
2.5 Reducible control-flow graphs
2.6 Reducibility and structured control
2.7 Further reading
Chapter 3 Non-local control
3.1 Subroutines for code reuse
3.2 Procedures and functions
3.3 Design dimensions and implementation strategies for functions
3.4 Control flow around function calls
3.5 Further reading
Chapter 4 Control inversion
4.1 Iterators
4.2 Generators
4.3 Coroutines and cooperative threads
4.4 Further reading
Part II Control operators for functional languages
Chapter 5 Functional languages
5.1 Declarative languages: getting rid of control?
5.2 XL: expressions and spreadsheets
5.3 APP: expressions and user-defined functions
5.4 FUN: functions as first-class values
5.5 Reductions under contexts
5.6 Further reading
Chapter 6 Continuations and the CPS transformation
6.1 Notion of continuation
6.2 Denotational semantics reminder
6.3 Continuation-based denotational semantics
6.4 Denotational semantics for labels and jumps
6.5 The CPS transformation
6.6 Semantic properties of the CPS transformation
6.7 Further reading
Chapter 7 Programming with continuations
7.1 Writing functions in CPS
7.2 Iterators
7.3 Asynchronous and concurrent programming
7.4 Errors and exceptions
7.5 Backtracking
7.6 Generating, filtering and counting
7.7 Further reading
Chapter 8 Control operators
8.1 Landin’s J operator
8.2 Call-with-current-continuation (callcc)
8.3 Implementing control structures with callcc
8.4 Semantics of callcc
8.5 Delimited continuations
8.6 Semantics of delimited continuation operators
8.7 Implementing control structures with delimited continuations
8.8 CPS transformation for delimited continuations
8.9 Further reading
Part III From exceptions to algebraic effects and handlers
Chapter 9 Exceptions
9.1 Programming with exceptions
9.2 Semantics of exceptions
9.3 ERS and CPS transformations for exceptions
9.4 Checked exceptions
9.5 Exception capabilities
9.6 Further reading
Chapter 10 Effect handlers for user-defined effects
10.1 From exceptions to effects
10.2 Effect handlers and delimited continuations
10.3 Control inversion
10.4 Cooperative multithreading
10.5 Semantics of effect handlers
10.6 CPS transformation for effect handlers
10.7 Further reading
Chapter 11 Monads
11.1 Commonalities in semantics and program transformations
11.2 Monads and the computational lambda-calculus
11.3 Examples of monads
11.4 The monadic transformation
11.5 Programming with monads
11.6 Further reading
Chapter 12 Algebraic effects
12.1 Generic semantics for monadic programs
12.2 Free monads
12.3 Algebra reminder
12.4 Monads as algebraic structures
12.5 A language of algebraic effects
12.6 Semantic effect handlers
12.7 A language of algebraic effects and handlers
12.8 Further reading
Part IV Reasoning about control and effects
Chapter 13 Type and effect systems
13.1 Type systems reminder
13.2 Simple types for advanced control structures
13.3 Issues with parametric polymorphism
13.4 A simple type and effect system for checked exceptions
13.5 Subtyping over effect types
13.6 Row polymorphism for effect types
13.7 A polymorphic type and effect system for algebraic effects
13.8 Limitations and extensions of row polymorphism
13.9 Further reading
Chapter 14 Hoare logic for control structures
14.1 Deductive verification reminder
14.2 Hoare logic: a program logic for structured control
14.3 Hoare logic for jumps
14.4 Hoare logic for coroutines and cooperative threads
14.5 Further reading
Chapter 15 Separation logic for control operators
15.1 Separation logic reminder
15.2 A separation logic for a functional-imperative language
15.3 A separation logic for callcc
15.4 A separation logic for linear undelimited continuations
15.5 A separation logic for effect handlers with linear continuations
15.6 Further reading
