Acronyme :
LIMD : "Logique, Informatique et Mathématiques Discrètes"Descriptif de l'équipe :
Le thème de recherche général de l’équipe est l’informatique mathématique, au sens du GDR Informatique Mathématique : l’équipe developpe donc des objets et méthodes mathématiques pour répondre à des problématiques issues des grandes questions informatiques.L’équipe s’est construite à partir du thème historique de la logique et de la théorie de la démonstration, puis elle a évolué vers la thématique des mathématiques discrètes et de l’analyse géométrique pour l’imagerie, enfin elle s’est ouverte dans les dernières années à la théorie des langages de programmation, aux catégories, aux systèmes de numération, à la théorie des nombres et à la complexité algorithmique.
Il faut également noter qu’au sein du LAMA, l’équipe LIMD joue un rôle d’interface entre mathématiques et informatique, ce qui se traduit par diverses collaborations traversant les frontières des équipes aussi bien en mathématiques fondamentales qu’appliquées.
Publications de l'équipe
Vous trouverez dans le fichier Publications la liste des publications de l'équipe pour la période 2014-2019.
LIMD
Travaux représentatifs
- Tom Hirschowitz. Familial monads and structural operational semantics. PACMPL, 3(POPL): 21 :1–21 :28, 2019.
T. Hirschowitz a proposé une nouvelle approche abstraite de la sémantique opérationnelle catégorique, une méthode standard pour décrire mathématiquement les langages de programmation, obtenant pour la première fois un résultat général de correction de la bisimulation modulo contexte, une méthode pour démontrer des équivalences de programmes. Ce résultat offre de nouvelles perspectives sur une question très difficile, sur laquelle les dernières avancées remontaient à 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.