Fondements du calcul, langages et compilation

A major area of computer science is the design and study of languages that allow us to describe computations or processes. In general, the aim is to abstract away from low-level computing devices (machines, biological systems, etc.) to provide programmers with high-level languages that are more structured, enjoy desirable properties (encapsulation, parametricity, total store ordering, etc.) and are generally easier to reason about. Obviously, this cannot be achieved without a formal semantics, which is nevertheless often lacking for various reasons. First, providing a mathematically sound and manageable semantics may sometimes require the development of new mathematical tools (e.g. domain theory). Second, the design of computer languages is often driven by the race for technological innovation (e.g. multicore or web programming), resulting in semantics that are partially undefined or defined by an implementation ; it is often impossible to provide a formal semantics that completely accounts for the oddities of the resulting languages. Third, even when the design of a language is carried out with semantics in mind, it is possible that advanced aspects of computation do not have an obvious semantics (e.g. with probabilistic, temporal or concurrent computations) ; here, we note that language design can actually drive the definition of satisfying semantics.

Our research tackles these three difficulties in various domains, designing, studying and using various languages. We are dealing with programming languages, concrete (e.g. OCaml, R, …) and abstract (e.g. lambda-calculi), for a wide range of paradigms including sequential, concurrent, probabilistic, and quantum computation. We are also interested in modeling languages that are used to describe physical and software systems in order to predict and test their behaviors or properties. Finally, we also consider domain specific languages such as query languages (e.g. SQL) and specification languages (e.g. UML/OCL) whose simplicity and restricted focus provide excellent opportunities for automated verification.

Publications: https://hal.science/LMF-LC