Photo Responsable

Thème de recherche SPI - Semantics, Proofs and Implementations

Chefe de Equipe :

Thérèse Hardin

Curta apresentação

Dessin Bulles HAL

The SPI team build formal tools for critical software. Two languages are released: - a higher-order synchronous language (Lucid Synchrone) with clock synthesis and several static analyses (initialization, typing, ...). - a language, called FOC, for specifications and programs, which allows to mix declarations, definitions, properties and proofs in a compilation unit. FOC has strong object features (inheritance, late binding) and an encapsulation mechanism. Proofs are currently done within Coq. The compiler produces OCaml sources, Coq sources and automatic documentation (XML files).

ATTENTION : L'organisation en thèmes n'existe plus depuis 2006, voir maintenant dans les équipes.



janeiro 1997 → dezembro 2003

Mentions légales
Mapa do site