Mots-clés
Équipe
CRI
Biographie
Olivier Hermant est un chercheur en informatique théorique et en logique mathématique, dont les travaux se concentrent sur l’automatisation du raisonnement, la preuve formelle et les systèmes de réécriture. Ses recherches abordent des thématiques variées telles que la déduction modulo, les méthodes de preuve par tableaux, la skolémisation, ou encore l’optimisation des infrastructures matérielles sous l’angle de la neutralité carbone. Il a contribué au développement d’outils comme le prouveur automatique Goéland, Zenon Modulo, ou encore Dedukti, un vérificateur universel de preuves. Ses travaux explorent également les liens entre sémantique algébrique (Heyting, pré-algèbres) et normalisation des preuves, ainsi que l’application de ces concepts à des logiques d’ordre supérieur ou à des théories axiomatiques comme la théorie des ensembles. Plus récemment, ses recherches ont intégré des problématiques liées à l’efficacité énergétique des systèmes informatiques et à la modélisation des impacts environnementaux des infrastructures numériques.
Publication(s)
-
2026
Investigations on Higher-Order Infinitary Logic DOI : 10.4230/LIPIcs.FSCD.2026.33
-
2026
Proceedings of the 21st Workshop on Logical Frameworks and Meta Languages: Theory and Practice DOI : 10.48550/ARXIV.2607.10318
-
2024
A Generic Deskolemization Strategy DOI : 10.29007/g1tm
-
2024
Optimizing the Impact of Upgrading Computer Equipment DOI : 10.1109/ICT4S64576.2024.00033
-
2020
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice DOI : 10.1007/s10817-019-09533-z
-
2019
Dependency pairs termination in dependent type theory modulo rewriting DOI : 10.4230/LIPIcs.FSCD.2019.9
-
2018
Runtime analysis of whole-system provenance DOI : 10.1145/3243734.3243776
-
2018
Polarized rewriting and tableaux in B set theory
-
2018
Consistency-Latency Trade-Off of the LibRe Protocol: A Detailed Study DOI : 10.1007/978-3-319-65406-5_4
-
2015
Managing Big Data with Information Flow Control DOI : 10.1109/CLOUD.2015.76
-
2015
Normalisation by completeness with heyting algebras DOI : 10.1007/978-3-662-48899-7_33
-
2014
Computing invariants with transformers: Experimental scalability and accuracy DOI : 10.1016/j.entcs.2014.08.003
-
2013
Semantic A-translations and super-consistency entail classical cut elimination DOI : 10.1007/978-3-642-45221-5_28
-
2013
Programming robots with events DOI : 10.1007/978-3-642-38853-8_2
-
2013
Using event-based style for developing M2M applications DOI : 10.1007/978-3-642-38027-3_37
-
2013
Polarizing double-negation translations DOI : 10.1007/978-3-642-45221-5_14
-
2013
Zenon modulo: When achilles outruns the tortoise using deduction modulo DOI : 10.1007/978-3-642-45221-5_20
-
2012
A simple proof that super-consistency implies cut elimination DOI : 10.1215/00294527-1722692
-
2012
The λΠ-calculus modulo as a universal proof language
-
2012
Unifying event-based and rule-based styles to develop concurrent and context-aware reactive applications: Toward a convenient support for concurrent and reactive programming
-
2012
A semantic proof that reducibility candidates entail cut elimination DOI : 10.4230/LIPIcs.RTA.2012.133
-
2011
Orthogonality and boolean algebras for deduction modulo DOI : 10.1007/978-3-642-21691-6_9
-
2011
Dynamic adaptation through event reconfiguration DOI : 10.1007/978-3-642-25126-9_78
-
2010
Completeness and cut-elimination in the intuitionistic theory of types - Part 2 DOI : 10.1093/logcom/exp076
-
2010
Resolution is cut-free DOI : 10.1007/s10817-009-9153-6
-
2008
A constructive semantic approach to cut elimination in type theories with axioms DOI : 10.1007/978-3-540-87531-414
-
2007
On constructive cut admissibility in deduction modulo DOI : 10.1007/978-3-540-74464-1_3
-
2007
A simple proof that super-consistency implies cut elimination DOI : 10.1007/978-3-540-73449-9_9
-
2006
A semantic completeness proof for TaMeD DOI : 10.1007/11916277_12
-
2005
Semantic cut elimination in the intuitionistic sequent calculus DOI : 10.1007/11417170_17
Enseignements
Développement de services mobiles (PI MOBAPP)
Projet (PI MOBAPP)
Période d'enseignement d'option (octobre+janvier)
Informatique fondamentale et compilation (Cours du TR ALTOS)
En « informatique fondamentale » : Introduction : langages et grammaires, notion de problème, systèmes logiques, formalisation des mathématiques et applications à l'informatique, limites de l'informatique, notion de résolution effective (incomplétude, décidabilité), modèles opératoires. Modèles de calcul : machines de Turing, notion de calculabilité, lambda-calcul, systèmes de réécriture, équations diophantiennes, thèse de Turing/Church, équivalences ; application aux paradigmes de programmation (impératif, fonctionnel, objet, logique). Définitions des langages de programmation : syntaxe, typage, notion de point fixe, sémantique opérationnelle (McCarthy, 1963), sémantique axiomatique (Hoare, 1969), sémantique dénotationnelle (Milne et Strachey, 1976). Complexité : types de complexité, non-déterminisme, complexité temporelle, problèmes NP-complets, théorème de Cook, complexité spatiale, théorèmes de hiérarchies. Aspects avancés : randomisation, informatique quantique, calcul ADN. La partie « compilation » exemplifiera les concepts abordés ci-dessus et mènera à une implémentation concrète d’un compilateur : Grammaires formelles. Analyse lexicale, analyse syntaxique et génération automatique de tels analyseurs. Arbres de syntaxe. Représentation intermédiaire. Génération de code assembleur.
Management des systèmes d'information (MSI) option
L'option MSI complète les enseignements de tronc commun et spécialisés pour maîtriser ces technologies : différents sujets techniques sont abordés selon les années. Citons par exemple la cryptographie, la sécurité des réseaux, les langages de script pour le développement rapide, les outils de gestion de sources, la compilation de langages informatiques, l'utilisation et la configuration de machines virtuelles, les systèmes distribués, etc. Une ouverture aux questions de management permet enfin de prendre conscience des difficultés de mise en œuvre concrète et efficace des technologies dans les systèmes d'information des organisations. Exemples de projets dans le cadre de l'option, en groupe ou individuels : développement d'une blockchain "MineCoin" analyse de traces de piratages avec de l'apprentissage artificiel développement d'un jeu 2D avec un moteur ad-hoc applications web de recommandation (finance, humour) application mobile de jeu en ligne attaques réseau par interception et modifications de paquets messagerie instantannée cryptographique système de sauvegarde à distance cryptographique partage de donné "cloud" réellement sécurisé algorithmes de filtrages sur carte graphique (GPU) analyse automatique de schémas de données Exemples de sujets d'option ces dernières années : classification par reconnaissance vocale et analyse sémantique (Deezer) analyses de données et prévisions du chiffre d'affaire (Datadog, NYC) intégration et optimisation des propositions de détours (Blablacar) développement d'un système de suivi des comportements clients (Pandacraft) développement d'effets visuels (Smart & Soft) audit de sécurité d'application Android (Solucom) tarification d'assurances avec des données géographiques (AXA) enrichissement cartographique de vues radar (THALES) haute disponibilité pour une base de donnée en mémoire (Quartet FS) analyse de la sécurité du protocole OpenFlow (ANSSI) système d'information pour Autolib (Polyconseil) analyse de données "big data" sur le marché aérien (AMADEUS) conception de cibles pour des tests radar (THALES) compilation et optimisation d'applications de traitement d'image (KALRAY) optimisation d'un système de cache de données distribué (AMADEUS, Allemagne) conception d'un espace client web (SopraGroup / LexisNexis) optimisation de la fourniture de contenu vidéo (Orange Lab) développement de jeux graphiques (Silicon Studio Corp, Japon) modèles d'architectures décisionnelles (Solucom) construction automatique de profils utilisateurs (Technicolor, USA) migration d'architectures serveurs vers le cloud (Samsung, Corée du Sud) système d'exploitation optimisé pour supercalculateur (CEA) application vidéo pour mobiles (TangoMe) détection de fraudes bancaires (Oresys) calculs de risques financiers (Société Générale) application de suivi de la production pétrolière (Accenture / Total) extension de l'interface Google Earth (Google, USA) instrumentation d'applications financières (CALYON, Japon)
Analyse des Langages (trimestre recherche)
Direction(s) de thèse(s)
- 2026 Transformations source à source prouvées pour l’architecture Arm MOREL Élian
- 2021 Mathématiques inversées des démonstrations Coq GERAN Yoan
- 2017 Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting GENESTIER Guillaume
- 2013 Automated Deduction and Proof Certification for the B Method HALMAGRAND Pierre
- 2013 Vérification de typage pour le λΠ-calcul modulo: théorie et pratique SAILLARD Ronan