Professor at the Computer Science and Engineering Department at University of Gothenburg.
coquand @ chalmers.se
3 talks given for the Autumn School "Proof and Computations" September 2024 part 1 and part 2 and part 3
Talk at the workshop on Inductive Definitions, Prague, May 2024 slides
Two talks given for the Summer School "Interactions of Proof Assistants and Mathematics" Regensburg, September 2023 part 1 and part 2
A talk for Marc Bezem's fest, August 2023
A general talk about Interactive Proof System, June 2023. This has been commented in an interesting way (especially the comment about the history of the notion of proof in mathematics) by Michael Harris. However, he fails to cite the important "But maybe the main interest of such tools is that they can help the mathematicians in organising thoughts and in getting better understanding".
A talk for Thorsten Altenkirch 60th birthday, October 2022
A talk about sheaf cohomology and univalent type theory, July 2022
A talk on dependent type theory and formalisation of mathematics, February 2022
A talk on canonicity and normalisation for dependent type theory, ITC, December 2021
A talk on Skolem-Noether Theorem, Dagsthul, December 2021
Some remarks on dependent type theory
A talk on the notion of potential infinity and sheaf models
A talk with some historical remarks about sheaf models and connections with Galois descent
A talk about algebraically closed field and sheaf models at the HOTTEST seminar
A talk about impredicativity given at the Graduate Student ITC seminar
A talk for the Oberwolfach seminar on Proof Theory anc Constructive Mathematics, November 2020, on constructive remarks about the theory of central simple algebras
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 Lorenzen's work, with an application to constructive measure theory (March 2018)
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 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.)