The contents of the TaPL/ATaPL book in jPDF Tweak bookmark format.

atapl-contents.txt

1;;Advanced Topics in Types and Programming Languages;1
2;;Preface;10
2;;I Precise Type Analyses;16
3;;1 Substructural Type Systems;18
4;;1.1 Structural Properties;19
4;;1.2 A Linear Type System;21
4;;1.3 Extensions and Variations;32
4;;1.4 An Ordered Type System;45
4;;1.5 Further Applications;51
4;;1.6 Notes;55
3;;2 Dependent Types;60
4;;2.1 Motivations;60
4;;2.2 Pure First-Order Dependent Types;65
4;;2.3 Properties;69
4;;2.4 Algorithmic Typing and Equality;71
4;;2.5 Dependent Sum Types;76
4;;2.6 The Calculus of Constructions;79
4;;2.7 Relating Abstractions: Pure Type Systems;86
4;;2.8 Programming with Dependent Types;89
4;;2.9 Implementation of Dependent Types;98
4;;2.10 Further Reading;101
3;;3 Effect Types and Region-Based Memory Management;102
4;;3.1 Introduction and Overview;102
4;;3.2 Value Flow by Typing with Labels;105
4;;3.3 Effects;117
4;;3.4 Region-Based Memory Management;121
4;;3.5 The Tofte–Talpin Type System;129
4;;3.6 Region Inference;138
4;;3.7 More Powerful Models for Region-Based Memory Management;142
4;;3.8 Practical Region-Based Memory Management Systems;148
2;;II Types for Low-Level Languages;152
3;;4 Typed Assembly Language;156
4;;4.1 TAL-0: Control-Flow-Safety;157
4;;4.2 The TAL-0 Type System;161
4;;4.3 TAL-1: Simple Memory-Safety;170
4;;4.4 TAL-1 Changes to the Type System;176
4;;4.5 Compiling to TAL-1;179
4;;4.6 Scaling to Other Language Features;182
4;;4.7 Some Real World Issues;187
4;;4.8 Conclusions;190
3;;5 Proof-Carrying Code;192
4;;5.1 Overview of Proof Carrying Code;192
4;;5.2 Formalizing the Safety Policy;197
4;;5.3 Verification-Condition Generation;202
4;;5.4 Soundness Proof;214
4;;5.5 The Representation and Checking of Proofs;219
4;;5.6 Proof Generation;229
4;;5.7 PCC beyond Types;231
4;;5.8 Conclusion;234
2;;III Types and Reasoning about Programs;236
3;;6 Logical Relations and a Case Study in Equivalence Checking;238
4;;6.1 The Equivalence Problem;239
4;;6.2 Non-Type-Directed Equivalence Checking;240
4;;6.3 Type-Driven Equivalence;242
4;;6.4 An Equivalence Algorithm;243
4;;6.5 Completeness: A First Attempt;247
4;;6.6 Logical Relations;248
4;;6.7 A Monotone Logical Relation;251
4;;6.8 The Main Lemma;252
4;;6.9 The Fundamental Theorem;254
4;;6.10 Notes;258
3;;7 Typed Operational Reasoning;260
4;;7.1 Introduction;260
4;;7.2 Overview;261
4;;7.3 Motivating Examples;262
4;;7.4 The Language;268
4;;7.5 Contextual Equivalence;276
4;;7.6 An Operationally Based Logical Relation;281
4;;7.7 Operational Extensionality;294
4;;7.8 Notes;303
2;;IV Types for Programming in the Large;306
3;;8 Design Considerations for ML-Style Module Systems;308
4;;8.1 Basic Modularity;309
4;;8.2 Type Checking and Evaluation of Modules;313
4;;8.3 Compilation and Linking;317
4;;8.4 Phase Distinction;320
4;;8.5 Abstract Type Components;322
4;;8.6 Module Hierarchies;332
4;;8.7 Signature Families;335
4;;8.8 Module Families;339
4;;8.9 Advanced Topics;353
4;;8.10 Relation to Some Existing Languages;356
4;;8.11 History and Further Reading;358
3;;9 Type Definitions;362
4;;9.1 Definitions in the Typing Context;366
4;;9.2 Definitions in Module Interfaces;373
4;;9.3 Singleton Kinds;382
4;;9.4 Notes;399
2;;V Type Inference;402
3;;10 The Essence of ML Type Inference;404
4;;10.1 What Is ML?;404
4;;10.2 Constraints;422
4;;10.3 HM(X);437
4;;10.4 Constraint Generation;444
4;;10.5 Type Soundness;449
4;;10.6 Constraint Solving;453
4;;10.7 From ML-the-Calculus to ML-the-Language;466
4;;10.8 Rows;475
2;;A Solutions to Selected Exercises;506
2;;References;550
2;;Index;582

tapl-contents.txt

1;B;Types and Programming Languages;1
2;I;Perface;13
2;B;1 Introduction;23
3;;1.1 Types in Computer Science;23
3;;1.2 What Type Systems Are Good For;26
3;;1.3 Type Systems and Language Design;31
3;;1.4 Capsule History;32
3;;1.5 Related Reading;34
2;B;2 Mathematical Preliminaries;37
3;;2.1 Sets, Relations, and Functions;37
3;;2.2 Ordered Sets;38
3;;2.3 Sequences;40
3;;2.4 Induction;41
3;;2.5 Background Reading;42
2;I;I Untyped Systems;43
3;B;3 Untyped Arithmetic Expressions;45
4;;3.1 Introduction;45
4;;3.2 Syntax;48
4;;3.3 Induction on Terms;51
4;;3.4 Semantic Styles;54
4;;3.5 Evaluation;56
4;;3.6 Notes;65
3;B;4 An ML Implementation of Arithmetic Expressions;67
4;;4.1 Syntax;68
4;;4.2 Evaluation;69
4;;4.3 The Rest of the Story;71
3;B;5 The Untyped Lambda-Calculus;73
4;;5.1 Basics;74
4;;5.2 Programming in the Lambda-Calculus;80
4;;5.3 Formalities;90
4;;5.4 Notes;95
3;B;6 Nameless Representation of Terms;97
4;;6.1 Terms and Contexts;98
4;;6.2 Shifting and Substitution;100
4;;6.3 Evaluation;102
3;B;7 An ML Implementation of the Lambda-Calculus;105
4;;7.1 Terms and Contexts;105
4;;7.2 Shifting and Substitution;107
4;;7.3 Evaluation;109
4;;7.4 Notes;110
2;I;II Simple Types;111
3;B;8 Typed Arithmetic Expressions;113
4;;8.1 Types;113
4;;8.2 The Typing Relation;114
4;;8.3 Safety = Progress + Preservation;117
3;B;9 Simply Typed Lambda-Calculus;121
4;;9.1 Function Types;121
4;;9.2 The Typing Relation;122
4;;9.3 Properties of Typing;126
4;;9.4 The Curry-Howard Correspondence;130
4;;9.5 Erasure and Typability;131
4;;9.6 Curry-Style vs. Church-Style;133
4;;9.7 Notes;133
3;B;10 An ML Implementation of Simple Types;135
4;;10.1 Contexts;135
4;;10.2 Terms and Types;137
4;;10.3 Typechecking;137
3;B;11 Simple Extensions;139
4;;11.1 Base Types;139
4;;11.2 The Unit Type;140
4;;11.3 Derived Forms: Sequencing and Wildcards;141
4;;11.4 Ascription;143
4;;11.5 Let Bindings;146
4;;11.6 Pairs;148
4;;11.7 Tuples;150
4;;11.8 Records;151
4;;11.9 Sums;154
4;;11.1 Variants;158
4;;11.11 General Recursion;164
4;;11.12 Lists;168
3;B;12 Normalization;171
4;;12.1 Normalization for Simple Types;171
4;;12.2 Notes;174
3;B;13 References;175
4;;13.1 Introduction;175
4;;13.2 Typing;181
4;;13.3 Evaluation;181
4;;13.4 Store Typings;184
4;;13.5 Safety;187
4;;13.6 Notes;192
3;B;14 Exceptions;193
4;;14.1 Raising Exceptions;194
4;;14.2 Handling Exceptions;195
4;;14.3 Exceptions Carrying Values;197
2;I;III Subtyping;201
3;B;15 Subtyping;203
4;;15.1 Subsumption;203
4;;15.2 The Subtype Relation;204
4;;15.3 Properties of Subtyping and Typing;210
4;;15.4 The Top and Bottom Types;213
4;;15.5 Subtyping and Other Features;215
4;;15.6 Coercion Semantics for Subtyping;222
4;;15.7 Intersection and Union Types;228
4;;15.8 Notes;229
3;B;16 Metatheory of Subtyping;231
4;;16.1 Algorithmic Subtyping;232
4;;16.2 Algorithmic Typing;235
4;;16.3 Joins and Meets;240
4;;16.4 Algorithmic Typing and the Bottom Type;242
3;B;17 An ML Implementation of Subtyping;243
4;;17.1 Syntax;243
4;;17.2 Subtyping;243
4;;17.3 Typing;244
3;B;18 Case Study: Imperative Objects;247
4;;18.1 What Is Object-Oriented Programming?  ;247
4;;18.2 Objects ;250
4;;18.3 Object Generators ;251
4;;18.4 Subtyping ;251
4;;18.5 Grouping Instance Variables ;252
4;;18.6 Simple Classes ;253
4;;18.7 Adding Instance Variables ;255
4;;18.8 Calling Superclass Methods ;256
4;;18.9 Classes with Self ;256
4;;18.1 Open Recursion through Self ;257
4;;18.11 Open Recursion and Evaluation Order ;259
4;;18.12 A More Efficient Implementation ;263
4;;18.13 Recap ;266
4;;18.14 Notes ;267
3;B;19 Case Study: Featherweight Java;269
4;;19.1 Introduction;269
4;;19.2 Overview;271
4;;19.3 Nominal and Structural Type Systems;273
4;;19.4 Definitions;276
4;;19.5 Properties;283
4;;19.6 Encodings vs. Primitive Objects;284
4;;19.7 Notes;285
2;I;IV Recursive Types;287
3;B;20 Recursive Types;289
4;;20.1 Examples;290
4;;20.2 Formalities;297
4;;20.3 Subtyping;301
4;;20.4 Notes;301
3;B;21 Metatheory of Recursive Types;303
4;;21.1 Induction and Coinduction;304
4;;21.2 Finite and Infinite Types;306
4;;21.3 Subtyping;308
4;;21.4 A Digression on Transitivity;310
4;;21.5 Membership Checking;312
4;;21.6 More Efficient Algorithms;317
4;;21.7 Regular Trees;320
4;;21.8 μ-Types;321
4;;21.9 Counting Subexpressions;326
4;;21.1 Digression: An Exponential Algorithm;331
4;;21.11 Subtyping Iso-Recursive Types;333
4;;21.12 Notes;334
2;I;V Polymorphism;337
3;B;22 Type Reconstruction;339
4;;22.1 Type Variables and Substitutions;339
4;;22.2 Two Views of Type Variables;341
4;;22.3 Constraint-Based Typing;343
4;;22.4 Unification;348
4;;22.5 Principal Types;351
4;;22.6 Implicit Type Annotations;352
4;;22.7 Let-Polymorphism;353
4;B;22.8 Notes;358
3;;23 Universal Types;361
4;;23.1 Motivation;361
4;;23.2 Varieties of Polymorphism;362
4;;23.3 System F;363
4;;23.4 Examples;366
4;;23.5 Basic Properties;375
4;;23.6 Erasure, Typability, and Type Reconstruction;376
4;;23.7 Erasure and Evaluation Order;379
4;;23.8 Fragments of System F;380
4;;23.9 Parametricity;381
4;;23.1 Impredicativity;382
4;;23.11 Notes;383
3;B;24 Existential Types;385
4;;24.1 Motivation;385
4;;24.2 Data Abstraction with Existentials;390
4;;24.3 Encoding Existentials;399
4;;24.4 Notes;401
3;B;25 An ML Implementation of System F;403
4;;25.1 Nameless Representation of Types;403
4;;25.2 Type Shifting and Substitution;404
4;;25.3 Terms;405
4;;25.4 Evaluation;407
4;;25.5 Typing;408
3;B;26 Bounded Quantification;411
4;;26.1 Motivation;411
4;;26.2 Definitions;413
4;;26.3 Examples;418
4;;26.4 Safety;422
4;;26.5 Bounded Existential Types;428
4;;26.6 Notes;430
3;B;27 Case Study: Imperative Objects, Redux;433
3;B;28 Metatheory of Bounded Quantification;439
4;;28.1 Exposure;439
4;;28.2 Minimal Typing;440
4;;28.3 Subtyping in Kernel F <:;443
4;;28.4 Subtyping in Full F <:;446
4;;28.5 Undecidability of Full F <:;449
4;;28.6 Joins and Meets;454
4;;28.7 Bounded Existentials;457
4;;28.8 Bounded Quantification and the Bottom Type;458
2;I;VI Higher-Order Systems;459
3;B;29 Type Operators and Kinding;461
4;;29.1 Intuitions;462
4;;29.2 Definitions;467
3;B;30 Higher-Order Polymorphism;471
4;;30.1 Definitions;471
4;;30.2 Example;472
4;;30.3 Properties;475
4;;30.4 Fragments of F ω;483
4;;30.5 Going Further: Dependent Types;484
3;B;31 Higher-Order Subtyping;489
4;;31.1 Intuitions;489
4;;31.2 Definitions;491
4;;31.3 Properties;494
4;;31.4 Notes;494
3;B;32 Case Study: Purely Functional Objects;497
4;;32.1 Simple Objects;497
4;;32.2 Subtyping;498
4;;32.3 Bounded Quantification;499
4;;32.4 Interface Types;501
4;;32.5 Sending Messages to Objects;502
4;;32.6 Simple Classes;503
4;;32.7 Polymorphic Update;504
4;;32.8 Adding Instance Variables;507
4;;32.9 Classes with “Self”;508
4;;32.1 Notes;510
2;I;Appendices;513
3;B;A Solutions to Selected Exercises;515
3;B;B Notational Conventions;587
4;;B.1 Metavariable Names;587
4;;B.2 Rule Naming Conventions;587
4;;B.3 Naming and Subscripting Conventions;588
2;B;References;589
2;B;Index;627