Acronym :

LIMD : "Logic, Computer Science, and Discrete Mathematics"

Team description :

Initially focused on logic and proof theory, the team was renamed "LIMD" in 2007, following its opening to new activities. The general topic is Mathematical Computer Science, as in the eponymous GDR IM, a CNRS research group: we develop mathematical objects and methods to address problems from computer science.

Within mathematical computer science, our main themes are Logic and Programming and Discrete Mathematics1.

Both themes have as central objects of study the notions of computation, programs, and algorithms, although considering them from various viewpoints: some of us work on the very concept of computing, others explore more algorithmic and programming questions.

Logic and Programming

Concerning proof theory and programming, our activity ranges from foundations to actual implementation of an experimental tool, PML, which is both a programming language and a proof assistant. On the foundational side, our focus is mainly on the Curry-Howard correspondence between proofs and programs, and its extensions to realisability. More generally, we work on programming languages, from their specification to their compilation. A central mathematical object in this theme is Church's λ-calculus.

Selected publications

Discrete mathematics

Our research in discrete mathematics revolves around a common range of objects (images, finite or infinite words, configurations, tilings, sub-shifts), but considering different issues, from their geometric understanding to the study of dynamic systems acting on them. Combinatorics on words (substitutions, Sturmian sequences, discrete straight lines, etc) provide a central tool for this research. On the conceptual side, a central question underlying our work is that of understanding the links between local constraints, or laws, and global configurations, or dynamic processes.

Selected publications

Add to these two themes the research activity of R. Bonnet (emeritus professor).