Professor at the Computer Science and Engineering Department at University of Gothenburg.
coquand @ chalmers.se
A talk given virtually at the HoTT seminar, CMU, September 2020, on sheaf models of type theory
An interview (in French) about my work for the "blog binaire" of the journal Le Monde
A talk in Munich (December 2019) about constructive sheaf models of type theory (some parts of this are j.w.w. Fabian Ruch)
A talk in Paris (September 2019) in honor of Pierre-Louis Curien
A talk about choice sequences in a univalent framework
A talk about univalent foundations at LICS 2018.
A general talk about univalent foundations (Hausdorff institute, Bonn, May 2018)
A talk about Lorenzen's work, with an application to constructive measure theory (March 2018)
A remark on the proof theoretic strength of univalence and some statements not provable from univalence (Oberwolfach, November 2017)
An adequacy theorem for partial type theory presented at the XXVth Agda implementer's meeting
Stack models of type theory, first in the groupoid case and then for cubical stacks
A presentation (meeting in Ljubljana on Syntax and Semantics of Type Theory) of the formalization of Mark Bickford of the cubical set model and of Chritisan Sattler's model structure on cubical sets. At the end, there are some general remarks about stacks for cubical sets
A presentation (in French) of Chritisan Sattler's model structure on cubical sets. The goal was only to spell out in details the definitions of the three classes of maps: cofibration, fibration and weak equivalence in this model
A talk in Leeds (July 2016) giving a survey of some works connected to cubical sets and univalence, presented at the workshop on Categorical Logic and Univalent Foundations
A talk in Marstrand (April 2016) giving some motivations for cubical type theory and slides of a corresponding talk of David Turner (May 1989)
A talk at a workshop in Stockholm (December 2015)
A talk at a workshop at IHES, Bures-sur-Yvette (November 2015)
A type system for cubical type theory. The following note should be close to a formalized version of this notion.
A talk for the conference Domain XII (Cork, August 2015) presenting the cubical set model of type theory. I tried to give the main idea how univalence and fibrancy of the universe are reduced to one operation on types.
A talk presenting a constructive model of univalence at the conference TYPES 2014
A talk at the last GDR informatique mathematique annual meeting, Paris January 2014
A lecture on Russell, Type Theory and Univalent Foundation
MALOA course on constructive algebra (Fischbachau, September 2010)
a survey talk given at ESOP, on functional programming and constructive mathematics
Summer School and Conference Mathematics, Algorithms and Proofs (MAP), August 11-29, 2008, Abdus Salam International Centre for Theoretical Physics, Trieste. You can access to my lecture notes from here
At the 2007 MAP meeting in Leiden, Harold Edwards presented a new addition formula for elliptic curves (directly inspired from Euler and Gauss). See here for a recent development. (To Chalmers CS Dept. Welcome page.)