Doctorant en Informatique Théorique

Université de Birmingham

Biographie

En ce moment, je suis en congé estival de l’université de Birmingham dans le cadre d’un stage de recherche chez Riverlane.

Lorsque je ne suis pas expatrié dans une startup cambridgienne - à distance depuis la sécurité de mon jardin à Biot, COVID oblige - je suis doctorant en seconde année dans l'équipe d’Informatique Théorique de l’Université de Birmingham. Mon directeur de thèse est Noam Zeilberger. Parmi les domaines de recherche qui m’attirent on peut trouver en vrac, la logique linéaire, la théorie des catégories appliquée, l’informatique quantique, les méthodes formelles ou encore la théorie des types.

Je suis diplômé d’un Master en Logique Mathématique et Fondements de l’Informatique (LMFI) de l’Université Paris Diderot. Durant cette formation, j’ai eu le privilège d’effectuer un stage de cinq mois au Laboratoire de Recherche en Informatique (LRI) de Paris Saclay sous la direction de Benoît Valiron. J’y ai développé la syntaxe et la sémantique d’un $\lambda\mu$-calcul probabiliste linéaire.

Lors de ma première année de doctorat, j’ai développé une théorie des polycatégories bifibrées. Je l’ai ensuite utilisée pour, à partir d’un foncteur dont le codomaine est un modèle de la logique linéaire, équiper le domaine d’une structure logique compatible avec celle du codomaine. Maintenant, en plus de continuer à étendre la théorie, je souhaiterai l’utiliser pour représenter des propriétés logiques de systèmes. L’idée sous-jacente est d’interpréter les systèmes par des catégories compactes fermées et leurs propriétés logiques par des catégories $\ast$-autonomes.

Intérêts

  • Catégories monoïdales
  • Logique Linéaire
  • Langages de Programmation Quantique

Formation

  • Doctorat en Informatique Théorique, 2021

    Université de Birmingham

  • Master en Logique Mathématique et Fondements de l'Informatique, 2016

    Université Paris Diderot

Articles récents

14 Choses à savoir sur les Polycatégories et leurs Fibrations

Une collection de choses à connaître sur les polycatégories, avec des pointeurs vers des articles pertinents. Quelques travaux inédits y sont présentés. Les polycatégories ont été définies par Szabo en 1975 dans l’article Polycategories. Les polycatégories sont des “catégories avec des morphismes à multiple entrées/sorties”. Les polycatégories interprètent le calcul des séquents classique de Gentzen. Les polycatégories se compose le long d’un objet. La composition de Polycatégories est analogue à la coupure en logique.

Projects

Conférences récentes

Bifibrations of polycategories and classical linear logic

Présentation de la théorie des polycatégories bifibrées et de leur lien avec la logique linéaire (en anglais)

Classical linear logic via bifibrations of polycategories

Une correspondance entre catégories linéairement distributives et polycatégories bifibrée sur la polycatégorie terminale. (en anglais)

Publications récentes

Bifibrations of polycategories and classical linear logic

Ceci est un article présenté à la conférence MFPS 2020. Il est aussi donné lieu à une présentation principale de la conférence ACT …

Experience

 
 
 
 
 

Research intern

Riverlane

Apr 2020 – Aug 2020 Cambridge, UK
Research on formal verification of quantum programs
 
 
 
 
 

Teaching Assistant

University of Birmingham

Oct 2018 – Actuellement Birmingham, UK
Teaching assistant for the following modules:

 
 
 
 
 

Formal methods software engineer

Clearsy Railway

Dec 2017 – Sep 2018 Paris, France

Software development for a CBTC (~8 months)

  • Vital (safety-critical) and non-vital onboard equipment: ATP and ATO
  • B Method (Formal Method), Ada and C
  • Formal proofs of properties verified by the software
  • Simulation and test of scenarios
  • Formation and supervision of new colleagues

Virtualisation and automation of all the generation/compilation process (~4months)

  • Interdependent VMs for Linux (CentOS), Windows (3.1, 10) and Solaris
  • Various languages used in the environment : B Method, C, Ada, Python, Bash
  • Vital programs compiled multiple times with different compilers
  • Communication with a License server
  • Creation of scripts for automation
  • Creation and configuration of a server to develop and test the project
 
 
 
 
 

Formal methods software engineer

Clearsy Railway

Jun 2017 – Sep 2018 Paris, France
Safety analysis of a SIL4 remote I/O platform (Software and micro-controller part)

  • Hazard and Risk Analysis
  • Safety Requirements Specification
  • Development of a Safety Demonstration based on the realization of the product
  • Documentation
  • Joint work with the Design team and the V&V team
  • Regular discussion with the certifier
  • Analysis of the full stack including formal methods, translators, compilers, communication protocols, micro-controllers
  • Standards : EN 50128, IEC 62279

Contact