- Labo: Verimag
- Area: Proofs of programs,
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:
- Previous works using Coq: