GALLIUM Research team
Programming languages, types, compilation and proofs
- Leader : Xavier Leroy
- Type : Project team
- Research center(s) : 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.
Research teams of the same theme :
- ANTIQUE - Static Analysis by Abstract Interpretation
- CAMBIUM - Programming languages: type systems, concurrency, proofs of programs
- CELTIQUE - Software certification with semantic analysis
- CONVECS - Construction of verified concurrent systems
- DEDUCTEAM - DEDUCTEAM
- GALLINETTE - Gallinette: developing a new generation of proof assistants
- MARELLE - Mathematical, Reasoning and Software
- MEXICO - Modeling and Exploitation of Interaction and Concurrency
- PARSIFAL - Proof search and reasoning with logic specifications
- PI.R2 - Design, study and implementation of languages for proofs and programs
- SUMO - SUpervision of large MOdular and distributed systems
- TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
- VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Search for a team
By Inria research center