You can find postscript versions of my talks.

Changing Data Representation within the Coq System: slides presented at TPHOLs'2003
Formalizing Square Matrices with Coq (Programming with Dependent Types): slides presented at TYPES'2003
Proving GMP Square Root within Coq: slides presented at "Séminaire des élèves ENS Lyon"
Abstracting Datatypes in the Calculus of Inductive Constructions: slides presented at TYPES'2000

Nicolas Magaud

Last modified: Wed Sep 17 17:43:57 MEST 2003