Till innehåll på sidan

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

Exportera till kalender

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.