Activity of the LIMD team

• The lab
  • Members
  • How to come
• Seminars
• Publications

• ---

• EDPs²
  • Research
  • Seminar
  • Publications

• ---

• Geometry
  • Research
  • Seminar
  • Publications

• ---

• LIMD
  • Research
  • Seminar
  • Publications

• ---

• Jobs offers
  • Permanent positions
  • Internships, PhD, Post-docs, ATER

• ---

• Workshops
• Scientific diffusion
• Teaching
• Internal

 

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 Mathematics¹.

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.

Publications de l'équipe

Vous trouverez dans le fichier Publications la liste des publications de l'équipe pour la période 2014-2019.

LIMD

Representative publications

• Tom Hirschowitz. Familial monads and structural operational semantics. PACMPL, 3(POPL): 21 :1–21 :28, 2019.
  
  T. Hirschowitz proposes an abstract framework based on category theory for operational semantics, a standard technique for mathematical modelling of programming languages. In this framework, he proves a correctness theorem for bisimulation up to context, a method for proving program equivalences, which is the first to cover cases with variable binding. This result opens new perspectives on a difficult question, mostly untouched since 2008.
  
  
• R.Bonnet and A. Leiderman « Countable Successor Ordinals as Generalized Ordered Topological Spaces » Topology and its Applications, Volume 241, 1 June 2018, pp. 197–202.
  
  Dans cet article, on généralise des résultats de E. van Douwen : nous caractérisons les ordinaux dénombrables comme étant les espaces topologiques dont toute image se plonge dans un espace ordonnable (la topologie est engendrée par les intervalles ouverts d’une chaîne).
  
  
• Pawel Gladkiet Krzysztof Worytkiewicz: Witt rings of quadratically presentable fields. Accepted for publication in "Categories and General Algebraic Structures with Applications", 2018.



• Jacques-Olivier Lachaud, David Coeurjolly et Jérémy Levallois. Robust and convergent curvature and normal estimators with digital integral invariants. In L. Najman et P. Romon, éditeurs. Modern Approaches to Discrete Curvature, volume 2184 de Lecture Notes in Mathematics, pages 293–348. Springer International Publishing, Cham, 2017.
  
  D. Coeurjolly, J.-O. Lachaud et J. Levallois ont proposé les premiers estimateurs de courbures moyenne, Gaussienne, et principales sur les surfaces digitales 3D, et qui ont la propriété prouvée de convergence [39, 13, 36, 37, 1]. Auparavant, seuls des estimateurs de courbure sur des contours 2D proposaient quelques garanties.
  
  
• C. Reutenauer and L. Vuillon, Palindromic Closures and Thue- Morse Substitution for Markoff Numbers, Uniform Distribution Theory, 2017
  
  L. Vuillon a travaillé avec C. Reutenauer (UQAM) sur la conjecture de Frobenius qui a maintenant plus de 100 ans d’âge dans cet article. Ils proposent une version combinatoire des mots de cette conjecture en utilisant la longueur de mots donnés par clôtures palindromiques itérées et la substitution de Thue-Morse pour définir les nombres de Markoff. Ces nombres interviennent en théorie des nombres et apparaissent dans la résolution de l’équation Diophantienne x2 + y2 + z2 = 3xyz. Etudier cette conjecture permettrait de mieux comprendre les propriétés de mauvaises approximations et la hiérarchisation des irrationnels quadratiques.
  
  
• N. Kayal, C. Saha et S. Tavenas, An Almost Cubic Lower Bound for Depth Three Arithmetic Circuits, Proceedings of International Colloquium on Automata, Languages, and Programming (ICALP), 33 :1–33 :15, 2016.
  
  Les auteurs exhibent un polynôme explicite et montrent que tout circuit arithmétique de profondeur trois qui le calcule nécessite une taille au moins presque-cubique. L’article a reçu le prix du meilleur article de la conférence.
  
  
• J.-O. Lachaud et B. Thibert. Properties of Gauss digitized shapes and digital surface integration. Journal of Mathematical Imaging and Vision, 54(2) :162-180, 2016.
  
  Cet article explicite les liens locaux et globaux entre surface d’un objet lisse eucliden et surface de cet objet discrétisé dans une grille régulière de pas h. La relation de projection est essentielle. Nous montrons qu’elle n’est pas bijective mais nous bornons la taille de sa partie non bijective. Nous montrons quand et où la surface discrétisée est une variété. Nous établissons ensuite la convergence multigrille d’une somme sur la surface discrétisée vers l’intégrale de surface correspondante. Tous ces résultats sont à la base du projet ANR « défis de tous les savoirs » CoMeDIC (2015–2020) et de la mise au point d’un opérateur de Laplace-Beltrami fortement convergent sur les surfaces digitales.
  
  
• Jean-Louis Verger-Gaugry: On the conjecture of Lehmer, limit Mahler measure of trinomials and asymptotic expansions. Unif. Distrib. Theory, 11:79–139, 2016.



• R. David et K. Nour. About range property for H. Logical Methods in Computer Science, vol. 10 (1 :3), pp. 1–18, 2014.
  
  La conjecture de Böhm sur la range property pour la théorie H stipule que le cardinal de l’image d’un λ-terme clos (vu comme une application modulo la théorie H) est soit 1 soit l’infini. Elle a résisté 42 ans avant que Polonsky trouve un contre-exemple. Nous proposons dans cet article une condition naturelle sur les λ-termes clos pour que le cardinal de leurs images soit toujours infini.
  
  
• R. David, C. Raffalli, P. Hyvernat et K. Nour ont publié leur livre « Les démonstrations mathématiques » sur l’apprentissage et l’enseignement des démonstrations mathématiques.
  
  
• Pierre Hyvernat. The size-change termination principle for constructor based languages. Logical Methods in Computer Science, 10(1), 2014.
  
  P. Hyvernat a étendu un test automatique (partiel) de terminaison pour prendre en compte la correction des définitions récursives impliquant des types coinductifs. C’est une première étape vers une solution au problème présent dans les langages de programmations avec type dépendants comme Agda, où la vérification des définition telle qu’elle est implémentée n’est pas correcte. Il est donc possible de « casser » le système. Ces travaux ont été l’objet de la conférence invitée au worshop PARIS (Oxford, printemps 2018) et ont été soumis.