Research Internships

A Ghost Sort in Rocq Feb. – Jul. 2024 (5.5 months)
Inria Nantes, Nantes (France)

Research internship under the supervision of Matthieu Sozeau and Théo Winterhalter.
Investigations of the implementation of a new proof-relevant yet computationally-irrelevant sort in the proof assistant Rocq. The interaction between this new sort and the existing sorts has naturally led to questions about elimination of inductives and the development of elimination constraints.
We plan on formalizing the meta-theory in MetaRocq and the relevant PRs will be linked once there is progress on this end.

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.