Type Systems Notes

Master
----+++ Description

Preliminary sketch, based on referenced book.


----+++ Topics

A selection from the
content taken from book (see Material, or http://www.cis.upenn.edu/~bcpierce/tapl).

   * I Untyped Systems 21
      * 3 Untyped Arithmetic Expressions 23
      * 4 An ML Implementation of Arithmetic Expressions 45
      * 5 The Untyped Lambda-Calculus 51
      * 6 Nameless Representation of Terms 75
      * 7 An ML Implementation of the Lambda-Calculus 83
   * II Simple Types 89
      * 8 Typed Arithmetic Expressions 91
      * 9 Simply Typed Lambda-Calculus 99
      * 10 An ML Implementation of Simple Types 113
      * 11 Simple Extensions 117
      * 12 Normalization 149
      * 13 References 153
   * III Subtyping 179
      * 15 Subtyping 181
      * 16 Metatheory of Subtyping 209
      * 17 An ML Implementation of Subtyping 221
      * 18 Case Study: Imperative Objects 225
      * 19 Case Study: Featherweight Java 247
   * IV Recursive Types 265
      * 20 Recursive Types 267
      * 21 Metatheory of Recursive Types 281
   * V Polymorphism 315
      * 22 Type Reconstruction 317
      * 23 Universal Types 339
      * 24 Existential Types 363
      * 26 Bounded Quantication 389
      * 27 Case Study: Imperative Objects, Redux 411
      * 28 Metatheory of Bounded Quantication 417
   * VI Higher-Order Systems 437
      * 29 Type Operators and Kinding 439
      * 30 Higher-Order Polymorphism 449
      * 31 Higher-Order Subtyping 467
      * 32 Case Study: Purely Functional Objects 475

and

   * Type classes

----+++ Material

   * Types and Programming Languages, Pierce, Benjamin C., ISBN: 0262162091
   * SL compiler with type inferencing for classes and datatypes

----+++ Dependencies

Requires ImplementationOfProgrammingLanguages


----+++ Lecturer

Main.DoaitseSwierstra, Main.AtzeDijkstra

----+++ History

none

----+++ Discussion