2018/2019

Homotopy Type Theory and Univalent Foundations

Mathematics

Principal investigators

Marc Bezem

Professor
University of Bergen (UiB)
Year at CAS

Bjørn Ian Dundas

Professor
University of Bergen (UiB)
Year at CAS

Abstract

Two central questions in the foundations of mathematics are: 'What is a proof?' and 'What does it mean to be equal?'

The answers to these questions vary enormously, both through time, but also from one culture to another. The modern mathematical proof may seem the most rigorous of all alternatives. Still, the ideal of well-documented, accountable knowledge, communicated with a proof certificate, is in no way reached. Typically, the validity of extremely complicated mathematical proofs is still supported only by the community's trust in peer review performed by a few acknowledged experts.

Since the modern society depends on mathematics, secure foundations are important. In the digital era we have powerful tools for verifying (and to some extent generating) formal mathematical proofs. The central challenge is finding a language that has sufficient expressive power, and at the same time can be mechanically processed in an efficient way. Homotopy type theory addresses exactly this challenge.

In this approach equality has a topological interpretation, yielding great flexibility. Our project aims at further exploring this novel foundation of mathematics, and apply it to verify some challenging mathematical theories.

Fellows

Benedikt Ahrens

Assistant Professor
University of Birmingham
Year at CAS

Kristian Alfsvåg

PhD Candidate
University of Bergen (UiB)
Year at CAS

Steve Awodey

Professor
Carnegie Mellon University
Year at CAS

Anthony Bordg

Postdoctoral Fellow
University of Cambridge
Year at CAS

Ulrik Buchholtz

Postdoctoral Fellow
Technical University of Darmstadt
Year at CAS

Thierry Coquand

Professor
Chalmers University of Technology & University of Gothenburg
Year at CAS

Peter Dybjer

Professor
Chalmers University of Technology & University of Gothenburg
Year at CAS

Daniel R. Grayson

Professor Em.
University of Illinois at Urbana-Champaign
Year at CAS

Kuen-Bang Hou (Favonia)

Assistant Professor
University of Minnesota
Year at CAS

Simon Huber

Postdoctoral Fellow
University of Gothenburg
Year at CAS

André Joyal

Professor Em.
Université du Québec à Montréal
Year at CAS

Chris Kapulkin

Assistant Professor
University of Western Ontario
Year at CAS

Peter LeFanu Lumsdaine

Assistant Professor
Stockholm University
Year at CAS

Paige North

Assistant Professor
Ohio State University
Year at CAS

Stefano Piceghello

PhD Candidate
University of Bergen (UiB)
Year at CAS

Emily Riehl

Assistant Professor
Johns Hopkins University
Year at CAS

Egbert Rijke

Postdoctoral Fellow
University of Illinois at Urbana-Champaign
Year at CAS

Christian Sattler

Postdoctoral Fellow
University of Gothenburg
Year at CAS

Floris van Doorn

Postdoctoral Fellow
Carnegie Mellon University
Year at CAS

News

‘CAS is such a fantastic institution,’ said mathematician and former CAS project leader Bjørn Ian Dundas when thinking back on his year at the Centre.

Events

2019

25

April
-
652, Georg Morgenstiernes Hus, University of Oslo