Person. Marc Bezem [marcbezem]

Professor of Computer Science
University of Bergen
https://www.ii.uib.no/~bezem/

Backlinks

Meeting. IAS Special Year on Univalent Foundations [ias-special-year]

2012
Steve Awodey, Thierry Coquand, Vladimir Voevodsky
Institute for Advanced Study

A Special Year on Univalent Foundations of Mathematics was held in 2012-13 at the Institute for Advanced Study, School of Mathematics, organized by Steve Awodey, Thierry Coquand, and Vladimir Voevodsky. The following people were the official participants:

Peter Aczel
Benedikt Ahrens
Thorsten Altenkirch
Steve Awodey
Bruno Barras
Andrej Bauer
Yves Bertot
Marc Bezem
Thierry Coquand
Eric Finster
Daniel Grayson
Hugo Herbelin
André Joyal
Daniel R. Licata
Peter LeFanu Lumsdaine
Assia Mahboubi
Per Martin-Löf
Sergey Melikhov
Alvaro Pelayo
Andrew Polonsky
Mike Shulman
Matthieu Sozeau
Bas Spitters
Benno van den Berg
Vladimir Voevodsky
Michael Warren
Noam Zeilberger

There were also the following students, whose participation was no less valuable.

Carlo Angiuli
Anthony Bordg
Guillaume Brunerie
Chris Kapulkin
Egbert Rijke
Kristina Sojakova

In addition, there were the following short- and long-term visitors, including student visitors, whose contributions to the Special Year were also essential.

Jeremy Avigad
Cyril Cohen
Robert Constable
Pierre-Louis Curien
Peter Dybjer
Martín Escardó
Kuen-Bang Hou (Favonia)
Nicola Gambino
Richard Garner
Georges Gonthier
Thomas Hales
Robert Harper
Martin Hofmann
Pieter Hofstra
Joachim Kock
Nicolai Kraus
Nuo Li
Zhaohui Luo
Michael Nahas
Erik Palmgren
Emily Riehl
Dana Scott
Philip Scott
Sergei Soloviev

Contributions

Reference. Type Theory with Explicit Universe Polymorphism [bezem-coquand-dybjer-escardó-2023]

July 28, 2023
Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
28th International Conference on Types for Proofs and Programs (TYPES 2022)
10.4230/LIPIcs.TYPES.2022.13

Reference. The univalence axiom in cubical sets [bch-2019]

August 1, 2019
Marc Bezem, Thierry Coquand, Simon Huber
Journal of Automated Reasoning
10.1007/s10817-018-9472-6

@article{bch-2019,
  author = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
  date = {2019-08-01},
  doi = {10.1007/s10817-018-9472-6},
  journaltitle = {Journal of Automated Reasoning},
  number = {2},
  pages = {159--171},
  title = {The Univalence Axiom in Cubical Sets},
  volume = {63},
}

Reference. A model of type theory in cubical sets [bch-2014]

2014
Marc Bezem, Thierry Coquand, Simon Huber
19th International Conference on Types for Proofs and Programs (TYPES 2013)

@inproceedings{bch-2014,
  author = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
  editor = {Matthes, Ralph and Schubert, Aleksy},
  address = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  url = {http://drops.dagstuhl.de/opus/volltexte/2014/4628},
  annotation = {Keywords: Models of dependent type theory, cubical sets, Univalent Foundations},
  booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  year = {2014},
  doi = {10.4230/LIPIcs.TYPES.2013.107},
  isbn = {978-3-939897-72-9},
  issn = {1868-8969},
  pages = {107--128},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{A Model of Type Theory in Cubical Sets}},
  volume = {26},
}