Formalizing Categories with Attributes in Coq

Speaker:

Peter Lumsdaine

Datum:

Son, 14/02/2016 - 17:00 - 17:45

Location:

MPIM Lecture Hall [2]

Parent event:

Workshop on Homotopy Type Theory [3]

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.