Underground Reading Group
Type Theory
Summer 2015 — Thursday, 2:30pm — CSE 203
Subscribe to the calendar: iCal or Google Calendar.| Date | Who | What |
|---|---|---|
|
Jun 25
11:00am-12:00pm
|
James W |
Elimination with a motive |
|
Jul 16
11:00am-12:00pm
|
—
|
Eliminating Dependent Pattern Matching |
|
Jul 23
11:00am-12:00pm
|
—
|
Observational equality, now! |
|
Jul 30
|
—
|
Innovations in computational type theory using Nuprl |
|
Aug 6
|
—
|
Intuitionistic Type Theory |
|
Aug 13
|
—
|
A Simplification of Girard’s Paradox |
|
Aug 20
|
—
|
Chapter 1 of Advanced Topics in Types and Programming Languages by Pierce |
|
Aug 27
|
—
|
A Polymorphic Modal Type System for Lisp-Like Multi-Staged Languages |
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.