Date Topic Read before class Project milestone Additional references
Sep Wed 3 Overview /
System F
TAPL 23  
  • Proofs and Types (1989), ch. 11
    Girard, Lafont, Taylor
    Cambridge University Press
  Mon 8 Existential types TAPL 24  
  Wed 10 Higher-order polymorphism TAPL 29-30 (except 30.5)
Groups and outline  
  Mon 15 Recursive types TAPL 20  
  Wed 17 Recursive types TAPL 21
   
  Mon 22 Recursive types TAPL 21    
  Wed 24 Logical Relations ATTAPL 2    
  Mon 29 Logical Relations ATTAPL 2    
Oct Wed 1 Typed Operational Reasoning ATTAPL 3 Related work  
  Mon 6 Contextual and ciu-equivalence ATTAPL 3    
  Wed 8 Logical equivalence ATTAPL 3    
  Mon 13 Fall Break      
  Wed 15 Using logical equivalence ATTAPL 3    
  Mon 20 Dependent Types ATTAPL 4   Functional Unparsing, Danvy
  Wed 22 Dependent Types ATTAPL 4   Lambda Calcluli with Types, Barendregt
  Mon 27 Effect types ATTAPL 5    
  Wed 29 Region-Annotated Language ATTAPL 5    
Nov

Mon 3

Tofte-Talpin Type System ATTAPL 5    
  Wed 5 Substructural Type Systems, Linearity ATTAPL 6    
  Mon 10 Algorithmic rules, extensions ATTAPL 6    
  Wed 12 Reference counts and ordered systems ATTAPL 6    
  Mon 17 Module systems
Determinancy, Abstraction and Sealing
ATTAPL 9.1-9.5    
  Wed 19 Avoidance problem, submodules, interface families ATTAPL 9.5-9.7    
  Mon 24 Functors ATTAPL 9.8-9.11 Technical material  
  Wed 26 Definitions in modules ATTAPL 10.1-10.2    
Dec Mon 1        
  Wed 3        
 

Mon 8

No lecture. Distribute project papers for peer comments.  

New deadline for final paper: Dec 15

 
Last modified: 11/26/03