GALLIUM Research team
Programming languages, types, compilation and proofs
- Leader : Xavier Leroy
- Research center(s) : CRI de Paris
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Proofs and Verification
The GALLIUM project-team conducts research on the design, formalization and implementation of programming languages and systems. Our objective is to improve the reliability of software systems through:
- higher-level, safer, more expressive programming languages based on the functional programming paradigm;
- automatic error detection via type systems and related static analyses;
- better linguistic support for formal methods, especially on-machine proofs of programs.
- Type systems, type inference, and related program analyses.
Static typing (the compile-time enforcement of a type system) is an effective way to detect large classes of programming errors early. Moreover, types provide additional structure both to individual programs and to programming language designs. Our ongoing research on type systems include: precise type-checking of data structures, including structural invariants, using generalized algebraic datatypes; partial type inference for advanced type systems, notably those featuring first-class and higher-order polymorphism; and type systems for programming "in the large" (modules, classes, mixins, etc).
- Formal verification of compilers and other programming tools.
When formal methods are applied to critical software to attain the highest levels of program certification, it becomes necessary to formally certify the tools that produce this software as well: compilers, static analyzers, etc. We are currently working on the development and formal verification, using the Coq proof assistant, of an optimizing compiler for the C programming language. The Coq development proves that the assembly code produced by this compiler has the same semantics as the source program. We are also interested in on-machine specification and verification of other programming tools, such as type systems.
- Design and implementation of high-level programming languages.
We develop the Objective Caml language and programming environment. Objective Caml is a high-level, statically-typed language that combines functional, imperative, object-oriented and modular programming. Our current plans for Caml and a possible successor design include reflections on unified mechanisms for modularization and parameterization of code fragments, on mechanisms for encapsulation and delimitation of state and imperative effects, and on application of recent advances in compilation and run-time systems.
- Software-proof co-design.
In contrast with the industry practice of formally verifying already written code that cannot be modified, we advocate and practice the simultaneous development of programs and of their correctness proofs. We are interested in ways to facilitate this "software-proof co-design" approach: enriching the programming power of logics such as Coq's, extending languages such as Caml with logical assertions, or contributing to new environments that integrate programming and proving. We also develop the Zenon automatic theorem prover as a core component of such environments.
International and industrial relations
- ANR advanced research action Compcert: compiler certification.
- Intel Corporation: implementation of the reFLect language.
- European IST project EDOS: environment for the development and distribution of Open Source software.
- Corporate members of the Caml Consortium.