Univalent Semantics of Constructive Type Theories

  • Vladimir Voevodsky
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)


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.

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Vladimir Voevodsky
    • 1
  1. 1.Institute for Advanced StudyPrincetonUSA

Personalised recommendations