ICMS 2016 Session: Univalent Foundations and Proof Assistants

ICMS 2016: Home, Sessions


Aim and Scope

The goal of the session is to bring together people in the proof assistant community working on the ideas inspired by the current activity surrounding the Univalence Axiom and, more generally, univalent foundations of mathematics and homotopy type theory. We expect to have representatives from several existent proof assistants as well as people working on the development of new type theories that will or may become the basis of proof assistants in the future. We consider the problem of developing the infrastructure that will allow formal specification and eventually verification of new proof assistants to be an important and possibly the most important one that is facing the community as the complexity of the type theories underlying the proof assistants grows and hope to also have talks from people and teams working in this direction.