Emmanuel Polonowski
Home
|
Teaching
|
Research
|
Programming
|
Version française
Programming
De Bruijn infrastructure Generation for Coq.
Generic Environments implementation in Coq.
LoopW: Certification of imperative programs and first-order classical logic.