Skip to main content

The Andromeda proof assistant

Posted in
Speaker: 
Andrej Bauer
Date: 
Sun, 14/02/2016 - 16:15 - 17:00
Location: 
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