Practical Foundations for Programming Languages

Preface......Page 3
I Judgements and Rules......Page 17
Judgements......Page 19
Inference Rules......Page 20
Derivations......Page 21
Rule Induction......Page 23
Iterated and Simultaneous Inductive Definitions......Page 25
Defining Functions by Rules......Page 27
Modes......Page 28
Exercises......Page 29
Derivability......Page 31
Admissibility......Page 33
Hypothetical Inductive Definitions......Page 35
Exercises......Page 37
Abstract Syntax Trees......Page 39
Abstract Binding Trees......Page 41
Parameterization......Page 46
Exercises......Page 47
Rule Schemes......Page 49
Generic Derivability......Page 50
Generic Inductive Definitions......Page 51
Parametric Derivability......Page 52
Exercises......Page 53
II Levels of Syntax......Page 55
Strings Over An Alphabet......Page 57
Lexical Structure......Page 58
Context-Free Grammars......Page 62
Grammatical Structure......Page 63
Ambiguity......Page 64
Exercises......Page 66
Hierarchical and Binding Structure......Page 67
Parsing Into Abstract Syntax Trees......Page 69
Parsing Into Abstract Binding Trees......Page 71
Exercises......Page 73
III Statics and Dynamics......Page 75
Syntax......Page 77
Type System......Page 78
Structural Properties......Page 80
Exercises......Page 82
Transition Systems......Page 83
Structural Dynamics......Page 84
Contextual Dynamics......Page 87
Equational Dynamics......Page 89
Exercises......Page 92
Type Safety......Page 93
Progress......Page 94
Run-Time Errors......Page 96
Exercises......Page 97
Evaluation Dynamics......Page 99
Relating Structural and Evaluation Dynamics......Page 100
Type Safety, Revisited......Page 101
Cost Dynamics......Page 103
Exercises......Page 104
IV Function Types......Page 105
Function Definitions and Values......Page 107
First-Order Functions......Page 108
Higher-Order Functions......Page 109
Evaluation Dynamics and Definitional Equivalence......Page 111
Dynamic Scope......Page 113
Exercises......Page 114
Gödel's System T......Page 115
Statics......Page 116
Dynamics......Page 117
Definability......Page 118
Non-Definability......Page 120
Exercises......Page 122
Plotkin's PCF......Page 123
Statics......Page 125
Dynamics......Page 126
Definability......Page 128
Exercises......Page 130
V Finite Data Types......Page 131
Product Types......Page 133
Nullary and Binary Products......Page 134
Finite Products......Page 135
Primitive and Mutual Recursion......Page 137
Exercises......Page 138
Binary and Nullary Sums......Page 139
Finite Sums......Page 141
Void and Unit......Page 142
Enumerations......Page 143
Options......Page 144
Exercises......Page 145
Pattern Matching......Page 147
Statics......Page 148
Dynamics......Page 150
Match Constraints......Page 152
Enforcing Exhaustiveness and Redundancy......Page 154
Checking Exhaustiveness and Redundancy......Page 155
Exercises......Page 156
Introduction......Page 157
Generic Extension......Page 158
Exercises......Page 161
VI Infinite Data Types......Page 163
Motivating Examples......Page 165
Types......Page 169
Dynamics......Page 170
Exercises......Page 171
Recursive Types......Page 173
Solving Type Isomorphisms......Page 174
Recursive Data Structures......Page 175
Self-Reference......Page 177
Exercises......Page 179
VII Dynamic Types......Page 181
The -Calculus......Page 183
Definability......Page 185
Scott's Theorem......Page 187
Untyped Means Uni-Typed......Page 189
Exercises......Page 191
Dynamically Typed PCF......Page 193
Variations and Extensions......Page 196
Critique of Dynamic Typing......Page 199
Exercises......Page 200
A Hybrid Language......Page 201
Optimization of Dynamic Typing......Page 203
Static ``Versus'' Dynamic Typing......Page 205
Reduction to Recursive Types......Page 206
VIII Variable Types......Page 207
Girard's System F......Page 209
System F......Page 210
Products and Sums......Page 213
Natural Numbers......Page 214
Parametricity Overview......Page 215
Predicative Fragment......Page 217
Prenex Fragment......Page 218
Rank-Restricted Fragments......Page 220
Exercises......Page 221
Abstract Types......Page 223
Statics......Page 224
Dynamics......Page 225
Data Abstraction Via Existentials......Page 226
Definability of Existentials......Page 228
Representation Independence......Page 229
Exercises......Page 231
Constructors and Kinds......Page 233
Statics......Page 234
Adding Constructors and Kinds......Page 236
Substitution......Page 238
Exercises......Page 241
Exercises......Page 243
IX Subtyping......Page 245
Subtyping......Page 247
Numeric Types......Page 248
Product Types......Page 249
Sum Types......Page 251
Sum Types......Page 252
Function Types......Page 253
Recursive Types......Page 254
Safety for Subtyping......Page 256
Exercises......Page 258
Singleton and Dependent Kinds......Page 259
Informal Overview......Page 260
X Classes and Methods......Page 263
Dynamic Dispatch......Page 265
The Dispatch Matrix......Page 267
Method-Based Organization......Page 269
Class-Based Organization......Page 270
Self-Reference......Page 271
Exercises......Page 273
Inheritance......Page 275
Subclassing......Page 276
Exercises......Page 279
XI Control Effects......Page 281
Machine Definition......Page 283
Safety......Page 285
Correctness of the Control Machine......Page 286
Soundness......Page 288
Exercises......Page 289
Failures......Page 291
Exceptions......Page 293
Exception Type......Page 294
Encapsulation......Page 296
Exercises......Page 298
Informal Overview......Page 299
Semantics of Continuations......Page 301
Coroutines......Page 303
Exercises......Page 307
XII Types and Propositions......Page 309
Constructive Logic......Page 311
Constructive Semantics......Page 312
Constructive Logic......Page 313
Rules of Provability......Page 314
Rules of Proof......Page 316
Propositions as Types......Page 317
Exercises......Page 318
Classical Logic......Page 319
Provability and Refutability......Page 320
Proofs and Refutations......Page 322
Deriving Elimination Forms......Page 324
Proof Dynamics......Page 326
Law of the Excluded Middle......Page 327
Exercises......Page 329
XIII Symbols......Page 331
Symbols......Page 333
Scoped Dynamics......Page 334
Scope-Free Dynamics......Page 335
Symbolic References......Page 337
Dynamics......Page 338
Exercises......Page 339
Statics......Page 341
Dynamics......Page 342
Type Safety......Page 343
Some Subtleties......Page 344
Fluid References......Page 347
Exercises......Page 348
Dynamic Classification......Page 349
Statics......Page 350
Safety......Page 351
Defining Dynamic Classes......Page 352
Classifying Secrets......Page 353
Exercises......Page 354
XIV Storage Effects......Page 355
Basic Commands......Page 357
Statics......Page 358
Dynamics......Page 359
Safety......Page 361
Some Programming Idioms......Page 363
Typed Commands and Typed Assignables......Page 365
Capabilities and References......Page 367
Exercises......Page 371
Mutable Data Structures......Page 373
Free Assignables......Page 374
Free References......Page 375
Safety......Page 376
Integrating Commands and Expressions......Page 378
Exercises......Page 381
XV Laziness......Page 383
Lazy Evaluation......Page 385
Need Dynamics......Page 386
Safety......Page 389
Lazy Data Structures......Page 392
Suspensions......Page 393
Exercises......Page 395
Polarization......Page 397
Polarization......Page 398
Focusing......Page 399
Statics......Page 400
Dynamics......Page 403
Safety......Page 404
Exercises......Page 405
XVI Parallelism......Page 407
Nested Parallelism......Page 409
Binary Fork-Join......Page 410
Cost Dynamics......Page 413
Multiple Fork-Join......Page 416
Provably Efficient Implementations......Page 418
Exercises......Page 422
Futures and Speculation......Page 423
Statics......Page 424
Statics......Page 425
Parallel Dynamics......Page 426
Applications of Futures......Page 429
Exercises......Page 431
XVII Concurrency......Page 433
Actions and Events......Page 435
Interaction......Page 437
Replication......Page 439
Allocating Channels......Page 441
Communication......Page 444
Channel Passing......Page 448
Universality......Page 450
Exercises......Page 452
Concurrent Algol......Page 453
Broadcast Communication......Page 456
Selective Communication......Page 458
Free Assignables as Processes......Page 461
Exercises......Page 462
Statics......Page 463
Dynamics......Page 466
Safety......Page 467
Exercises......Page 468
XVIII Modularity......Page 469
Exercises......Page 471
Basic Modules......Page 473
Parameterized Modules......Page 475
XIX Equivalence......Page 477
Equational Reasoning for T......Page 479
Observational Equivalence......Page 480
Extensional Equivalence......Page 484
Extensional and Observational Equivalence Coincide......Page 485
General Laws......Page 488
Induction Law......Page 489
Exercises......Page 490
Observational Equivalence......Page 491
Extensional Equivalence......Page 492
Extensional and Observational Equivalence Coincide......Page 493
Compactness......Page 496
Co-Natural Numbers......Page 499
Exercises......Page 501
Overview......Page 503
Observational Equivalence......Page 504
Logical Equivalence......Page 506
Parametricity Properties......Page 512
Representation Independence, Revisited......Page 515
Exercises......Page 517
XX Appendices......Page 519
Families of Sets......Page 521