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