Close

‹ Back to the directory

Olivier Hermant

Olivier Hermant

Professor

Center · CRI

Discipline(s)
Computer Science
Topic(s)
Computer Science

Keywords

Team

CRI

Biography

Olivier Hermant is a researcher in theoretical computer science, formal methods and mathematical logic, whose work focuses on the automation of reasoning, formal proof, and rewriting systems. His research addresses a variety of topics, such as modulo deduction, table-based proof methods, Skolemization, and the optimization of hardware infrastructure from the perspective of carbon neutrality. He has contributed to the development of tools such as the Goéland automated proof system, Zenon Modulo, and Dedukti, a universal proof verifier. His work also explores the connections between algebraic semantics (Heyting, prealgebras) and proof normalization, as well as the application of these concepts to higher-order logics or axiomatic theories such as set theory. More recently, his research has incorporated issues related to the energy efficiency of computer systems and the modeling of the environmental impacts of digital infrastructure.

Publication(s)

Teaching

Mobile Service Development (PI MOBAPP)

Course Director

Project (PI MOBAPP)

Course Director

Elective Course Period (October and January)

Course Director

Fundamentals of Computer Science and Compilation (TR ALTOS Course)

Course Director

In “Fundamental Computer Science”: Introduction: languages and grammars, the concept of a problem, logical systems, the formalization of mathematics and its applications to computer science, the limits of computer science, the concept of effective resolution (incompleteness, decidability), operational models. Computational models: Turing machines, the concept of computability, lambda calculus, rewriting systems, Diophantine equations, the Turing–Church thesis, equivalences; applications to programming paradigms (imperative, functional, object-oriented, logical). Definitions of programming languages: syntax, typing, the concept of a fixed point, operational semantics (McCarthy, 1963), axiomatic semantics (Hoare, 1969), denotational semantics (Milne and Strachey, 1976). Complexity: types of complexity, nondeterminism, time complexity, NP-complete problems, Cook’s theorem, space complexity, hierarchy theorems. Advanced topics: randomization, quantum computing, DNA computing. The “compilation” section will illustrate the concepts discussed above and lead to a concrete implementation of a compiler: Formal grammars. Lexical analysis, syntactic analysis, and automatic generation of such parsers. Syntax trees. Intermediate representation. Assembly code generation.

Information Systems Management (ISM) track

Course Director

The MSI track complements the core and specialized coursework to provide students with a thorough understanding of these technologies: various technical topics are covered depending on the academic year. Examples include cryptography, network security, scripting languages for rapid development, source code management tools, computer language compilation, the use and configuration of virtual machines, distributed systems, and more. Finally, an introduction to management issues helps students understand the challenges of effectively implementing these technologies in organizations’ information systems. Examples of projects within the track, either group or individual: development of a “MineCoin” blockchain; analysis of hacking traces using machine learning; development of a 2D game with a custom engine; web-based recommendation applications (finance, humor); mobile online gaming app; network attacks via packet interception and modification; cryptographic instant messaging; cryptographic remote backup system; truly secure “cloud” data sharing; filtering algorithms on graphics processing units (GPUs); automatic analysis of data schemas Examples of elective topics from recent years: classification using speech recognition and semantic analysis (Deezer); data analysis and revenue forecasting (Datadog, NYC); integration and optimization of detour suggestions (Blablacar); development of a customer behavior tracking system (Pandacraft); development of visual effects (Smart & Soft); Android application security audit (Solucom); insurance pricing using geographic data (AXA); map-based enhancement of radar views (THALES); high availability for an in-memory database (Quartet FS); security analysis of the OpenFlow protocol (ANSSI); information system for Autolib (Polyconseil); analysis of “big data” on the airline market (AMADEUS); design of targets for radar testing (THALES); compilation and optimization of image processing applications (KALRAY); optimization of a distributed data caching system (AMADEUS, Germany); design of a web-based customer portal (SopraGroup / LexisNexis) optimization of video content delivery (Orange Lab) development of graphics-based games (Silicon Studio Corp, Japan) decision-making architecture models (Solucom) automatic construction of user profiles (Technicolor, USA) migration of server architectures to the cloud (Samsung, South Korea) operating system optimized for supercomputers (CEA) mobile video application (TangoMe) detection of banking fraud (Oresys) financial risk calculations (Société Générale) oil production monitoring application (Accenture / Total); Google Earth interface extension (Google, USA); financial application instrumentation (CALYON, Japan)

Language Analysis (Research Quarter)

Course Director

PhD supervision

  • 2026 Transformations source à source prouvées pour l’architecture Arm MOREL Élian
  • 2021 Reversed Mathematics of Coq Proofs 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