Professor at the Computer Science and Engineering Department at University of Gothenburg.
coquand @ chalmers.se
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 note presenting in an internal way the uniform Kan operation. This suggest the following typing system. The following note should be close to a formalized version of this notion.
Some course notes presenting a cubical set model of type theory, with a presentation of a cubical syntax, which corresponds to an actual implementation
A talk presenting a constructive model of univalence at the conference TYPES 2014
A course on univalent foundation, CIRM, April 2014
A talk at the meeting on Proofs, Functions and Construction, Tuebingen February 2014
A talk at the last GDR informatique mathematique annual meeting, Paris January 2014
A talk on the Univalent Foundation given at a Royal Society International meeting on computational content of proofs
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.)