Ulrik Buchholtz: Weak dependent type theories
Time: Fri 2015-07-03 15.00 - 16.00
Location: Room 306, building 6, Kräftriket, Department of mathematics, Stockholm university
Participating: 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.