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 |
Re-read 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 |
Re-read 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 third-order logic
- Higher-order unification 30 years later
- A Formulae-as-Types Notion of Control –
call/ccis double-negation elimination????
Contact James W (jrw12@cs) if you want to get on the mailing list. Or subscribe yourself.