Underground Reading Group
Type Theory
Winter 2016 — Thursday, 2:30pm — CSE 203
Subscribe to the calendar: iCal or Google Calendar.| Date | Who | What |
|---|---|---|
|
Jan 7
|
James W Room: CSE 624
|
Organizational meeting |
|
Jan 14
|
Doug Room: CSE 203
|
Observational Equality Now |
|
Jan 21
|
—
Room: CSE 624
|
TBD |
|
Jan 28
|
Alex Room: CSE 624
|
A Formulae-as-Types Notion of Control |
|
Feb 4
|
Sam Room: CSE 203
|
Turing-Completeness Totally Free |
|
Feb 11
|
Bartosz Room: CSE 203
|
Category Theory intro - Part 1 of Bartosz’s blog |
|
Feb 18
|
Konstantin Room: CSE 303
|
From Sets to Types to Categories to Sets |
|
Feb 25
|
– Room: CSE 203
|
No meeting |
|
Mar 3
|
Nate and ?? Room: CSE 203
|
Type Theory in Type Theory using Quotient Inductive Types |
Paper Suggestions
-
Programming with Intersection Types and Bounded Polymorphism
-
Cubical Type Theory: a constructive interpretation of the univalence axiom
Contact James W (jrw12@cs) if you want to get on the mailing list. Or subscribe yourself.