Skip to main content

The UniMath project

Posted in
Dan Grayson
Sun, 2016-02-14 13:30 - 14:15
MPIM Lecture Hall

Implementations and formalizations

The focus of this session will be on computational aspects of homotopy
type theory and univalent foundations. Speakers will demonstrate, on the
one hand, formalizations of mathematics in the general-purpose proof
assistant Coq, and on the other, implementations of more experimental
type systems that have arisen directly from the homotopy type theory and
univalent foundations programme.


© MPI f. Mathematik, Bonn Impressum & Datenschutz
-A A +A