Research
- Labo: Verimag
- Team: Distributed and Complex Systems
- Area: Proofs of programs,
Formal methods,
Semantics of programming languages.
- Formalisms: Refinement calculus, Type theory.
- Issues: Combination of programming paradigms,
Refinement, Modularity, Inheritance, Applications of dependent types.
- Tools: Coq, Caml, B,
Lucid Synchrone.
- Previous works:
- FOC: specifying,
programming and proving Computer Algebra libraries.
-
Lucid Synchrone in Coq: a synchronous denotational semantics for
synchronous programming languages in type theory.
|