Jul 29 2013
Apr 30 2013
On Tuesday 30/04/2013, at 10h, in room Byron Blanc.
Speaker: Yves Bertot.
Title: Introduction to homotopy type theory.
Homotopy theory is an offspring of algebraic topology that makes it possible to sort topological spaces in equivalence classes and to study their algebraic properties. Since 2006, connections have been discovered between this theory and type theory, more precisely with respect types used to represent equality.
In this talk, I will describe some of these connection and show how new kinds of data-structures, called higher inductive types start to have a meaning in this context, and how they can be simulated in a simple extension of the Coq system.
Mar 19 2013
Mar 12 2012
Event: International Spring School on Formalization of Mathematics – MAP 2012.
Date: March 12–16, 2012.
Location: Sophia Antipolis, France.