Name

tapl, short stand for Types and Programming Languages.

Building

make all

Running

make bot target=test

Book Contents

Preface x

• 1 Introduction 1
• 2 Mathematical Preliminaries 15

I Untyped Systems 21

• 3 Untyped Arithmetic Expressions 23 (arith)
• 4 An ML Implementation of Arithmetic Expressions 45 (arith)
• 5 The Untyped Lambda-Calculus 51 (fulluntyped)
• 6 Nameless Representation of Terms 75 (fulluntyped)
• 7 An ML Implementation of the Lambda-Calculus 83 (untyped) and fulluntyped

II Simple Types 89

• 8 Typed Arithmetic Expressions 91 (tyarith)
• 9 Simply Typed Lambda-Calculus 99 (fullsimple)
• 10 An ML Implementation of Simple Types 113 (simplebool)
• 11 Simple Extensions 117 (fullsimple) and letexercise
• 12 Normalization 149
• 13 References 153 (fullref)
• 14 Exceptions 171 (fullerror)

III Subtyping 179

• 15 Subtyping 181 (fullsub) and rcdsubbot
• 16 Metatheory of Subtyping 209 (rcdsubbot) and bot
• 17 An ML Implementation of Subtyping 221
• 18 Case Study: Imperative Objects 225 (fullref)
• 19 Case Study: Featherweight Java 247

IV Recursive Types 265

• 20 Recursive Types 267 (fullisorec) and fullequirec
• 21 Metatheory of Recursive Types 281 (equirec)

V Polymorphism 315

• 22 Type Reconstruction 317 (recon) and fullrecon and reconbase
• 23 Universal Types 339 (fullpoly) and fullomega
• 24 Existential Types 363 (fullpoly)
• 25 An ML Implementation of System F 381
• 26 Bounded Quantification 389 (fullfsub) and fullfomsub
• 27 Case Study: Imperative Objects, Redux 411 (fullfsub)
• 28 Metatheory of Bounded Quantification 417 (fullfsub) and purefsub

VI Higher-Order Systems 437

• 29 Type Operators and Kinding 439 (fullomega)
• 30 Higher-Order Polymorphism 449 (fomega) and fullomega
• 31 Higher-Order Subtyping 467 (fomsub) and fullfomsub
• 32 Case Study: Purely Functional Objects 475 (fullupdate)