-
The CtCoq System: Design and Architecture
We present issues that arose in the design of the CtCoq user-interface for proof development. Covered issues include multi-processing, data display, mouse interaction,... -
A certified Compiler for an Imperative Language
This paper describes the process of mechanically certifying a compiler with respect to the semantic specification of the source and target languages. The proofs are... -
Preuves de systèmes réactifs dans le modèle synchrone
Stage de DEA. Rapport de stage.
