In this team, the theoretical research (mostly in Type Theory, computability, semantics of sequentiality and of parametricity) is pursued with the purpose of applications to programming language design and semantics, in particular functional, logic, equational and object oriented programming languages. Models of computation are also developed.
Multi-paradigm Languages
We consider the programming styles mentioned above as complementary approaches: each of them has suitable features to treat and solve certain kind of problems. Thus, one of our aims is the integration of some of the various features and styles above, in particular, we look for an integration of equational and functional languages, on one side, and equational and object oriented on the other.
Typing
Most of our work relies on foundational and technical tools derived from logic, such as recursion theory, proof theory, category theory and linear logic. This theoretical background clarifies many key aspects of typing and compiling and, by this, it permits to prove properties of programs. As a matter of fact, in programming languages, types (a notion originated in logic) introduced a remarkable, though partial form of correctness proof.
Mobility
Some techniques, also inspired by typing, are used for languages with mobility. These languages are designed for programming in large scale computer networks (such as Internet) and are still at an early experimental stage. We study their foundations and development with regards, in particular, to the security problems, as these properties, and their automatic verification, are today a categorical imperatif in view of the enormous growth of Web.
Geometry and Cognition, since 2001
A new research theme is also being developed. It concerns the relations between human cognition and the foundation of mathematics and computing. The current focus is on the "geometric organization of space". More precisely, the problem of space and of its mathematical intelligibility is a crucial issue since long in physics; it is a more recent scientific challenge in biology. It happens that the distribution of agents, as well as their interaction and spatial organisation, is a key issue in (distributed) computing as well. Finally, the focus on spatial invariants is to be considered a foundational theme for mathematics, largely disregarded by the prevailing tradition in logic. An interdisciplinary action is thus pursued. It first focuses on the geometric organization of physical and biological space, it should later be concerned with foundational problems in mathematics and computing (see the CenECC and its activities, an interdepartmental center of ENS, which includes among its founders a member of the team: http://www.lps.ens.fr/~risc/cenecc/)