Research
 Labo: Verimag
 Area: Proofs of programs,
Formal methods,
Semantics of programming languages, Verified compilation.
 Formalisms: Abstract Interpretation, Refinement calculus, Type theory.
 Issues: Combination of programming paradigms,
Refinement, Modularity, Inheritance, Parametricity, Applications of dependent types,
Certification of verification tools, Result (or lightweight) certification.
 Related Tools:
OCaml,
Coq,
CompCert,
Atelier B,
FoCaLiZe,
FramaC,
Lucid Synchrone,
Verasco,
Why
 Previous works using Coq:
