高等研究院原定于12月12日下午4：00举行的杰出学人讲座因故取消，给大家造成的不便，请谅解！

清华大学高等研究院

Institute for Advanced Study, Tsinghua University

杰出学人讲座

Distinguished Scholar Lectures

Professor Vladimir Voevodsky

Fields Medalist（2002年菲尔兹奖获得者）

Institute for Advanced Study（普林斯顿高等研究院）

Title：Univalent Semantics of Constructive Type Theories

时间：2011年12月12日（星期一）下午4:00

地点：清华大学科学馆高等研究院一楼报告厅

In this talk I will outline a new semantics for dependent polymorphic type theories with Martin-Lof identity types. It is based on a class of models which interpret types as simplicial sets or topological spaces defined up to homotopy equivalence. The intuition based on the univalent semantics leads to new answers to some long standing questions of type theory providing in particular well-behaved type theoretic definitions of sets and set quotients. So far the main application of these ideas has been to the development of “native” type-theoretic foundations of mathematics which are implemented in a growing library of mathematics for proof assistant Coq. On the other hand the computational issues raised by the univalent semantics may lead in the future to a new class of programming languages.