Professor at the Computer Science and Engineering Department at University of Gothenburg.
coquand @ chalmers.se
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
Course in type theory, introduction to the Univalent Foundation lecture 1, lecture 2,lecture 3, lecture 4
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.)