Research Internships

Correlation Between Models of GATs and Their Two Sortification Sept. 2025 – Mar. 2026 (6 months)
École Polytechnique, LIX, Inria, Palaiseau (France)

Research internship under the supervision of Ambroise Lafont.
Study of the categorical models of Generalized Algebraic Theories as an initial object in the 2-category of cartesian categories with a chosen exponential arrow. Formalization of the project in Rocq.

Bounded Sort Polymorphism in Rocq and Metarocq Feb. – Jul. 2025 (5.5 months)
Inria Nantes, Nantes (France)

Research internship under the supervision of Matthieu Sozeau and Théo Winterhalter.
Study of the theory of bounded sort polymorphism, restricting the type system of the proof assistant Rocq to get back the principal type property when activating sort polymorphism. Implementation of this type system in Rocq and start of the formalization of sort polymorphism in MetaRocq.
Investigations of the implementation of a new proof-relevant yet computationally-irrelevant sort in Rocq, following Théo’s work on a Ghost Type Theory.

Analyzing Proof-Terms in HoTT May – Jul. 2024 (3 months)
Chalmers University of Technology, Göteborg (Sweden)

Research internship under the supervision of Thierry Coquand.
Investigation of the computational properties of Egbert Rijke’s proof that there is a finite number of connected components in the type of groups of fixed cardinal.
Implementation of a bunch of standard results of homotopy type theory, as well as this proof in postt, for a total of a little over 9000 lines of code. The code is browsable over here.

Skolemization in First-Order Logic Jun. – Jul. 2023 (2 months)
Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier (LIRMM), Montpellier (France)

Research internship under the supervision of Julie Cailler, David Delahaye, Olivier Hermant and Simon Robillard.
Implementation of different versions of the Skolemization rule in a tableau-based automated theorem prover, Goéland.
Investigations about the certification of the different tableaux proofs obtained through interactive theorem provers, such as Coq.
Led to the publication of an article in LPAR-25.

Convex Hull in Interval Graphs Jun. – Jul. 2022 (2 months)
Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier (LIRMM), Montpellier (France)

Research internship under the supervision of Stéphane Bessy.
Exploration of the complexity of the convex hull problem in undirected interval graphs.

Automated Proofs in First-Order Logic Oct. 2021 – Aug. 2022 (11 months)
Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier (LIRMM), Montpellier (France)

Research project under the supervision of Hinde Bouziane, Julie Cailler, David Delahaye and Simon Robillard.
Implementation of deduction modulo theory and its variations as well as a typing system with rank-1 polymorphism in an automated theorem prover: Goéland.
Implementation of a Coq proof output for the tool, taking into account deduction modulo theory’s rewrite rules.

Von Neumann’s Architecture Jul. – Aug. 2021 (2 months)
Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier (LIRMM), Montpellier (France)

Research internship under the supervision of Arnaud Virazel.
Development of a simulator of Von Neumann’s architecture in JavaScript and vue.js for Computer Science’s first year course at Université de Montpellier “Architecture des Ordinateurs”. The code is available on GitLab.

An Efficient Unification ProcedureJun. 2021 (1 month)
Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier (LIRMM), Montpellier (France)

Research internship under the supervision of Hinde Bouziane, Julie Cailler and David Delahaye.
Modification and improvement of Voronkov’s abstract subsumption machine over terms in first-order logic to unify efficiently multiple terms. Implementation of the resulting data structure and procedure in Goéland, a first-order automated theorem prover.

Industry Internships

Developer and SysAdmin Summer 2019 and 2020 (5 months)
Techniques Numériques Expertise, Palavas-les-Flot (France)

Conception and development of a puzzle-game from scratch:

• Front-end desktop and mobile application.
• Back-end API and database.
• Online forms for dynamic management of the system.

Company’s system and databases administrator.

Web Developer Nov. 2019 – Apr. 2020 (6 months)
Faculté de Pharmacie de Montpellier, Montpellier (France)

Development of a website for the IDOUM (Innovative Decentralized and low cost treatment systems for Optimal Urban wastewater Management Project) research project as part of a mini-project as a freshman in computer science.