The Univalent Foundations Seminar will meet Wednesdays and Thursdays 11 – 12:30 in S-101 beginning 9.26.2012. See http://www.math.ias.edu/seminars for all currently scheduled IAS talks, and the calendar page here for the UF talks.
There are sometimes some additional seminars on Friday 11 – 12:30 in S-101
Notes for Vladimir seminars are available here: expressions_current.pdf and Universe polymorphic type sytem.pdf.
Monday April 15: TBA (Sergei Mehlikov)
Wednesday April 17: Linear type theory (Michael Warren)
Thursday April 18: Survey of results (The homotopy group)
Monday April 8: The semi-simplicial universe (Thierry Coquand) Wednesday April 10: The category of hSets (Bas Spitters) Thursday April 11: HoTT is a polyvalent foundation of mathematics (André Joyal)
Friday March 29: Revisiting the categorical interpretation of dependent type theory (Pierre-Louis Curien) Thursday March 28: Natural models of type theory (Steve Awodey) Wednesday March 27: The James construction and pi4(S^3)_ (Guillaume Brunerie)
Thursday March 21: Substructural type theory (Noam Zeilberger) Wednesday March 20: A proof assistant prototype based on algebraic effects and handlers (Andrej Bauer)
Friday March 15: W-types in SSets (Benno van den Berg) Thursday March 14: Homotopy colimits and a descent theorem (Egbert Rijke) Wednesday March 13: Eilenberg–MacLane spaces in HoTT (Dan Licata)
Thursday March 7: Setoids, e-categories and exact completions (Richard Garner) Wednesday March 6: Cohomology in HoTT (Eric Finster)
Friday March 1: Cartesian closed bicategories of bimodules (Nicola Gambino) Thursday February 28: Formal Abstract Homotopy Theory (Jeremy Avigad) Wednesday February 27: Semantics of higher inductive types (Mike Shulman)
Friday February 22: The Universe is Indiscrete (Martin Escardo) Thursday February 21: Locally Cartesian Closed Infinity Categories (Joachim Kock) Wednesday February 20: pi2(S^2) in HoTT_ (Guillaume Brunerie)
Thursday February 14: On finite types that are not h-sets (Sergey Mehlikov) video Wednesday February 13: The Hopf fibration in HoTT (Peter Lumsdaine) video
Thursday February 7: The structure identity principle (Peter Aczel) video Wednesday February 6: A Quillen model structure in HoTT (Peter Lumsdaine) video
Friday February 1: Weak infinity groupoids II (Guillaume Brunerie) Thursday January 31: Calculus of opetopes (Eric Finster) video Wednesday January 30: Weak infinity groupoids (Guillaume Brunerie) video
Thursday January 24: Orthogonal factorization systems in HoTT (Egbert Rijke) notes video Wednesday January 23: Homotopy and Univalence (Thorsten Altenkirch) video
Thursday January 17: State of the new proof assistant (Dan Grayson) video Wednesday January 16: Semi-simplicial types: what and why? (Peter Lumsdaine) video
Thursday December 20: Building HITs in realizability models (Andrej Bauer)
Friday December 14: A formalisation of semi-simplicial types, and some general issues about definitional equality (Hugo Herbelin)
Thursday December 13: Invariance under isomorphism and definability (Per Martin–Löf) video Wednesday December 12: The univalence axiom for simplicial diagrams (Mike Shulman) video
Friday December 7: TS + OCAML + LF (Dan Grayson) Thursday December 6: The simplicial set model (Peter Lumsdaine) Wednesday December 5: Type Systems VII (Vladimir Voevodsky)
Friday November 30: The game model (Peter Dybjer) slides video Thursday November 29: The simplicial set model (Chris Kapulkin) video Wednesday November 28: Type Systems VI (Vladimir Voevodsky) Description of LF in TS style video
Wednesday November 21: Type Systems V (Vladimir Voevodsky) video
Friday November 16: pik(S^n) for k < n_ (Guillaume Brunerie) Thursday November 15: The simplicial set model (Peter Lumsdaine) video Wednesday November 14 (1:30 – 3): Type Systems IV (Vladimir Voevodsky) Wednesday November 14: Towards implementing Higher Inductive Types (Mike Shulman) notes video
Friday November 9: Ssreflect methodology for large-scale (Assia Mahboubi) Thursday November 8: The simplicial set model (Peter Lumsdaine) Wednesday November 7: Informal HoTT (collective) wiki page and semi-simplicial types (Peter Lumsdaine) wiki page
Friday October 26: Universes in Type Theory (Zhaohui Luo) slides Thursday October 25: The simplicial set model (Peter Lumsdaine)
Thursday October 18: Toward a computational interpretation of Univalence (Dan Licata) video
Thursday October 11: On the setoid model of type theory (Erik Palmgren) slides video Wednesday October 10: Type Systems III (Vladimir Voevodsky) video
Friday October 5: Type Theories as representable maps of presheaves (Steve Awodey) notes Thursday October 4: Univalent Foundations in Coq (Michael Warren) video Wednesday October 3: Type Systems II (Vladimir Voevodsky) video
Wednesday September 26: Type Systems I (Vladimir Voevodsky) video
Here are some proposed topics for future seminars, perhaps with speakers: