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 |
Implementing mathematics with the NuPRL proof development system
Programming with Intersection Types and Bounded Polymorphism
call/cc
is double-negation elimination????Contact James W (jrw12@cs) if you want to get on the mailing list. Or subscribe yourself.