Professor at the Computer Science and Engineering Department at University of Gothenburg.
coquand @ chalmers.se
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.)