 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 |