GT Mathématiques Discrètes, Logique et Vérification
Le groupe de travail Mathématiques Discrètes, Logique et Vérification
regroupe des enseignants-chercheurs du LIM, un chercheur associé, des doctorants et des stagiaires
autour de thèmes liés aux mathématiques discrètes, à la logique et à la vérification :
- Youssef Boudabbous (25)
- Christian Delhommé (25)
- Christian Espindola (25)
- Alexandre Mansard (27)
- Fred Mesnard (27)
- Marianne Morillon (25)
- Étienne Payet (27)
- Sirine Boudabbous, doctorante en informatique
- Grégoire Grondin, doctorant en mathématiques
- Thierry Marianne, doctorant en informatique
- Pierre Jaffuer, M2 université de La Réunion, 2022/2023
- Nicolas Lhost, M2 université de Namur, Belgique, 2022/2023
- Malika Moussa, M2 université de La Réunion, 2020/2021
- Marin Ricros, M2 ENS Cachan, 2020/2021
Les chercheurs d'autres horizons sont les bienvenus pour exposer leurs idées sur ces thèmes.
Liste des interventions
30/11/2023 : Kristof Kanalas (Masaryk University, Tchéquie)
Rasiowa-Sikorski lemmas and the completeness of infinitary first-order logic
31/10/2023 : Fred Mesnard
Discussion sur les liens possibles entre la preuve de programme logique et les idées présentées par Karim Nour
26/10/2023 : Karim Nour (université de Chambéry)
Proofs and programs
20/10/2023 : Karim Nour (université de Chambéry)
A termination proof in typed lambda-calculus
28/09/2023 : Kristof Kanalas (Masaryk Universty, Tchéquie)
The small object argument
07/09/2023 : Kristof Kanalas (Masaryk Universty, Tchéquie)
Logique catégorique et catégoricité
09/05/2023 : David Holgate (Western Cape University, Afrique du Sud)
An ordered view of continuous maps
20/04/2023 : Nicolas Lhost (M2 université de Namur, Belgique)
Une interface SMT-LIB pour ISO-Prolog
13/04/2023 : Fausto Spoto (Université de Vérone, Italie)
An Overview of Blockchain Technology
06/04/2023 : Étienne Payet
Non-terminaison (présentation de travaux en cours, deuxième partie)
23/03/2023 : Pierre Jaffuer (M2 université de La Réunion)
Un protocole de retour à la base pour robots mobiles
09/03/2023 : Étienne Payet
Non-terminaison (présentation de travaux en cours, première partie)
02/03/2023 : Nicolas Lhost (M2 université de Namur, Belgique)
Présentation du solveur SMT Z3
08/12/2022 : Thierry Marianne (doctorant LIM)
Quelques preuves en LPTP
24/11/2022 : Christian Delhommé
Discussion au sujet d'une collaboration avec Lyon suivie par une discussion scientifique informelle
10/11/2022 : Christian Espindola
Objet ordinal
03/11/2022 : Fred Mesnard
Preuves interactives de programmes en LPTP
27/10/2022 : Fred Mesnard
Preuves interactives de programmes en LPTP
24/02/2022 : Fred Mesnard
Suite de la présentation de l’article Formal verification of logic programs: foundations and implementation de Robert Stärk
10/02/2022 : Fred Mesnard
Présentation de l’article Formal verification of logic programs: foundations and implementation de Robert Stärk
09/12/2021 : Christian Espindola
Présentation de l’article Five stages of accepting constructive mathematics de Andrej Bauer
29/10/2021 : Christian Delhommé
Bases de Gröbner III
22/10/2021 : Christian Delhommé
Bases de Gröbner II
15/10/2021 : Christian Delhommé
Bases de Gröbner I
07/10/2021 : Fred Mesnard
Coq (deuxième partie)
30/09/2021 : Fred Mesnard
Coq (première partie)
23/09/2021 ; Christian Espindola
Théorème de Morley en logique infinitaire
08/07/2021 : Youssef Boudabbous
Différents modes de reconstruction, décomposition modulaire et dualité des digraphes
30/06/2021 : Marin Ricros (M2 ENS Cachan)
Transducteur sur les arbres
17/06/2021 : Fred Mesnard
Etat de l'art concernant la terminaison de boucles linéaires/entières
08/06/2021 : Christian Delhommé et Etienne Payet
Fonctions de rang, paires de dépendance
20/05/2021 : Malika Moussa (M2 université de la Réunion)
Paires de dépendance
29/04/2021 : Fred Mesnard
Size-Change Termination et contraintes de monotonicité
01/04/2021 : Fred Mesnard
Approches globales/locales pour la preuve de terminaison
11/03/2021 : Christian Delhommé
Le théorème de Ramsey
04/02/2021 : Étienne Payet
Présentation informelle de la programmation logique
