Ulrik Buchholtz: Weak dependent type theories
Tid: Fr 2015-07-03 kl 15.00 - 16.00
Plats: Room 306, building 6, Kräftriket, Department of mathematics, Stockholm university
Medverkande: Ulrik Buchholtz, Carnegie-Mellon University
I'll discuss ongoing work on formulating proof-theoretically weak dependent type theories (of strength polytime and primitive recursive) that permit some higher type and large eliminations. Motivations include constructive reverse mathematics and eventually also a weak homotopy type theory.