Gallium

Scientific research

The research conducted in the Gallium group aims at improving the safety, reliability and security of software through advances in programming languages and formal verification of programs. Our work is centered on the design, formalization and implementation of functional programming languages, with particular emphasis on type systems and type inference, formal verification of compilers, and interactions between programming and program proof. The Caml language and the CompCert verified compiler embody many of our earlier research results. Our work spans the whole spectrum from theoretical foundations and formal semantics to applications to real-world problems.

Programming languages: design, formalization, implementation
Type systems
Compilation
Interface with formal methods

See also: Grants and contracts

Research topics

• Programming languages
• Type systems
• Compilation
• Formal methods

See also

• Grants and contracts
• Gagallium blog