GALLIUM Research team
Programming languages, types, compilation and proofs
- Leader : Xavier Leroy
- Type : Project team
- Research center(s) : Paris - Rocquencourt
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Programs, Verification and Proofs
Team presentationThe 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.
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 :
- ABSTRACTION - Abstract Interpretation and Static Analysis
- ATEAMS - Analysis and Transformation based on rEliAble tool coMpositionS
- CARTE - Theoretical adverse computations, and safety
- CASSIS - Combination of approaches to the security of infinite states systems
- CELTIQUE - Software certification with semantic analysis
- COMETE - Concurrency, Mobility and Transactions
- CONTRAINTES - Constraint programming
- DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
- FORMES - Formal Methods for Embedded Systems
- MARELLE - Mathematical, Reasoning and Software
- MEXICO - Modeling and Exploitation of Interaction and Concurrency
- PAREO - Formal islands: foundations and applications
- PARSIFAL - Proof search and reasoning with logic specifications
- PI.R2 - Design, study and implementation of languages for proofs and programs
- PROSECCO - Programming securely with cryptography
- SECSI - Security of information systems
- SPECFUN - Symbolic Special Functions : Fast and Certified
- SUMO - SUpervision of large MOdular and distributed systems
- TASC - Theory, Algorithms and Systems for Constraints
- TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
- VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
This team follows
Search for a team
By Inria research center