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
-
Tom Hirschowitz and Xavier Leroy, Mixin modules in a
call-by-value setting, ACM Transactions on Programming Languages
and Systems, 27(5) :857-881, 2005
This paper presents a type system for call-by-value mixin modules. It also contains the first interpretation of call-by-value mixin modules in terms of recursive definitions.
- Peter Hancock and Pierre Hyvernat, Programming
interfaces and basic topology, Annals of Pure and
Applied Logic, Volume 137, Issues 1-3 : 189-239, 2006
Formal topology is a constructive approach to standard topology. In a very different setting, the notion of "interaction structure" is used to formalise component-oriented programming. This paper connects these two worlds (topology and programming), defining an equivalence of categories between the spaces of formal topology with continuous functions as morphisms, and interfaces with simulations as morphisms.
- René David and Karim Nour, An
arithmetical proof of the strong normalization for the
lambda-calculus with recursive equations on types,
TLCA 2007, LNCS 4583 : 84-101, 2007
This paper provides a purely combinatorial proof of strong normalisation for the simply typed λ-calculus with mutually recursive equations on types satisfying the Mendler conditions (shown by Mendler to be necessary and sufficient for strong normalisation). Mendler's proof of strong normalisation uses reducibility candidates, and is not formalisable in first order logic. So, our proof shows that the strength of the considered system is weaker than that of Peano arithmetic.
- Christophe Raffalli
Realisability of the axiom of choice in HOL. (An analysis of
Krivine’s work), Fundamenta Informaticae vol. 84
tome 2, 241-258, 2008
This paper is an introduction to recent work in realisability, mainly Jean-Louis Krivine's work on realising the axiom of choice. We also show how to optimise the extracted programs, distinguishing formulas with and without algorithmic contents. Indeed, some care is needed in adapting the optimisation techniques from intuitionnistic realisability to the the classical case.
- Christophe Raffalli and Pierre
Hyvernat PML
and
its goals
PML is both a functional programming language and proof assistant, featuring a common language for types, proofs, and programs. This unification goes beyond the standard paradigms of proofs as programs and propositions as types, replacing them with programs as types and propositions and proofs.
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
- Jacques-Olivier
Lachaud, Anne Vialard, François de Vieilleville, Fast, accurate
and convergent tangent estimation on digital contours,
Image and Vision Computing, Volume 25, Issue 10 : 1572-1587, 2007
We introduce the first local geometrical estimator on discrete contours proved to be asymptotically convergent. We show that it can be computed in time linear in the size of the data. We further demonstrate that it behaves in practice better than the others, even at low scale, according to various criteria (mean and maximal quadratic errors, isotropy, conservation of convexity properties, continuity).
- G. Paquin and L. Vuillon,
A
characterization of balanced episturmian sequences,
Electronic Journal of Combinatorics, Vol 14, no 1, Research
Paper 33, 12 pp, 2007
Fraenkel pretends that the only infinite word (on k letters), balanced on each of its letters and having letter frequencies all different one from another, is the infinite word (Frk)ω so that Frk = Frk−1 k Frk−1 with Fr3=1213121. This speculation is now 35 years old, and a first step towards its resolution has been done thanks to the study of balanced sequences given by a guiding sequence. During a three months' stay in Montreal (Canada), L. Vuillon finalized this paper with G. Paquin about the Fraenkel speculation for episturmian periodic words. This result demonstrates the Fraenkel speculation for a sub-class of balanced sequences (which generalize the Sturm words, i.e. the sequences given by discrete approximation of a straight line in the plane). It is an important step forward, because we think we'll be able to come down to this sub-class to resolve the speculation.
- L. Boyer and G. Theyssier On Local
Symmetries and Universality in Cellular Automata,
STACS 2009, 26th International Symposium on Theoretical Aspects of
Computer Science, (electronic proceedings)
For various families of cellular automata defined by local symmetries, we have shown that the density of the intrinsic universality in the family equals 1. One of the main improvements is to obtain the result for any way of making the pair radius / number of states tend to infinity. The hypothesis of local symmetries are also very simple and for some of them (totalistic automata) often studied in the literature.
- 1
- Add to these two themes the research activity of R. Bonnet (emeritus professor).