Underground Reading Group
Type Theory
Autumn 2015 — Thursday, 2:30pm — CSE 203
Subscribe to the calendar: iCal or Google Calendar.Date  Who  What 

Oct 1

James W 
In Search of Types (optional) Organizational meeting 
Oct 8

James W Room: CSE 674

Skim introduction; Read Chapter 1, Sections 1 through 7 For background on the simply typed lambda calculus, see Chapter 9 of Pierce’s Types and Programming Languages (there is a copy in the lab and several of us have copies). 
Oct 15

Konne 
Finish Chapter 1 
Oct 22

Pavel 
Reread 1.12 on equality Take a look at the first part of Pavel’s blog post on equality. 
Oct 29

Doug Woooooos 
Chapter 2 through and including 2.3 
Nov 5

John Toman 
Reread 2.2 and 2.3 
Nov 12

Pavel Panchekha 
2.4–2.5 
Nov 19

– 
No meeting (PLDI deadline) 
Nov 26

– 
No meeting (Thanksgiving) 
Dec 3

James W 
2.6–2.9 
Dec 10

James W 
finish chapter 2 
Paper Suggestions
 Constructive mathematics and computer programming

Implementing mathematics with the NuPRL proof development system
 Chapters from TAPL or ATTAPL?

Programming with Intersection Types and Bounded Polymorphism
 The undecidability of unification in thirdorder logic
 Higherorder unification 30 years later
 A FormulaeasTypes Notion of Control –
call/cc
is doublenegation elimination????
Contact James W (jrw12@cs) if you want to get on the mailing list. Or subscribe yourself.