Works on GnuCOBOL at OCamlPro

I contributed to the GnuCOBOL open source C transpiler for COBOL since 2024 and I helped OCamlPro fixing bugs on the compiler.

• List of my contributions

I contributed to the SuperBOL Studio VSCode extension for COBOL. It has been developed in OCaml and features a modern LSP for COBOL.

• List of my contributions

Independent research

Computational foundations of logic

I (slowly) develop the theory of Girard’s transcendental syntax with other ReFL members and I’m also trying to develop tools and programs.

Stellogen programming language

I develop Stellogen, an experimental programming language based on Girard’s transcendental syntax.

It is a minimalistic and logic-agnostic programming language based on term unification. It draws inspiration (or try to draw inspiration) from Prolog (unification-based computation), Smalltalk (message-passing, object-oriented programming, minimalism), Coq (proof-as-program paradigm, iterative programming with tactics), Scheme/Racket (minimalism and metaprogramming), Haskell/Ruby (for their syntax).

Presentations

• Introduction à la Géométrie de l’Interaction. ReFL seminar, February 2023 (online), 35min.

Past academic research

PhD thesis in computer science / mathematical logic

I was a PhD student at Université Sorbonne Paris Nord from 2019 to June 2024, supervised by Thomas Seiller and Damiano Mazza.

Title: “An exgesis of transcendental syntax”

Abstract. This thesis provides a clarification of Girard’s recent work entitled “transcendental syntax”. Girard suggests a reorganisation and a reinterpretation of concepts of mathematical logic coming from his previous works on linear logic, proof-nets, ludics and geometry of interaction. Unlike the approaches of semantic explanations based on the linguistic nature of logical entities and their evaluation, transcendental syntax suggests to start from the notion of computation as primitive in order to reconstruct mathematical logic, by starting with the proof-nets of linear logic. […]

I also had some reflections on the relation between the computational complexity of (lambda-)terms and Turing machines and boolean circuits (invariance thesis) in the context of implicit computational complexity (ICC) with Damiano Mazza but I mainly worked with Thomas Seiller on deciphering Jean-Yves Girard last project of “transcendental syntax” proposing a new computational foundation for logic based on its works on linear logic (and more especially proof-net theory).

• PhD manuscript
• Slides of the defense

Other presentations

• Transcendental Syntax: a toolbox for the interface logic-computation. GT Scalp. November 2021 Fontainbleau, 20min.
• A technical reading of the Transcendental Syntax. LDP Seminar. September 2021 Marseille, 90min.
• Entretien de suivi de thèse. September 2021 Villetaneuse, 30min.
• A gentle introduction to Girard’s Transcendental Syntax. TLLA 2021, June 2021 Roma (online), 15min. [Extended abstract]
• From computation to a reconstruction of (linear) logic. Midlands Graduate School 2021, April 2021 Midlands (online), 10-15min.
• Transcendental Syntax - The dynamics of logic programs and tilings, applied to Linear Logic. LIPN Seminar, March 2021 Villetaneuse (online), 70-80min.
• A taste of Girard’s Transcendental Syntax. Workshop Proof-Nets, January 2021 Montpellier (online), 20min.

Teaching at Université Sorbonne Paris Nord

2022—2023

192 hours (ATER position)

• Programmation 1, TD/TP (L1 Mathématique-informatique):
  C language
• Programmation Orientée Objet, TP (L2 Informatique):
  OO programming in Java
• Spécifications algébriques et test logiciel, TD (L2 Informatique):
  proof methods, proof by induction on lists and trees, formal specifications
• Programmation logique, TD (Sup Galilée 2):
  logic programming with Prolog
• Programmation 2, TP (L1 Mathématique-informatique):
  recursion, memoisation, pointers, arrays, structures, sort algorithms
• Initiation web, TP (L1 Informatique):
  HTML, CSS
• Systèmes & réseaux, TP (L2 Informatique):
  processes, threads, synchronization, sockets
• Programmation distribuée, TP (M1 Informatique):
  sockets, client-server, concurrent and distributed programming in Java

2021—2022

64 hours

• Programmation 1, TD/TP (L1 Mathématique-informatique):
  C language
• Calculabilité & Décidabilité, TD (L3 Informatique):
  Turing machines, computability, diagonalization, complexity theory

2020—2021

64 hours

• Programmation 1, TD/TP (L1 Mathématique-informatique):
  C language
• Fondements de la programmation, TD (M1 Informatique):
  sequential and parallel abstract machines, lambda-calculus, Turing machines
• Programmation fonctionnelle, TD (L2 Informatique):
  lambda-calculus, fixpoint operators, simple types, unification algorithm, type inference

Université Sorbonne Paris Nord (2019-2020)

64 hours

• Informatique 1, TD/TP (L1 Physique-Chimie & sciences pour l’ingénieur):
  C language
• Informatique 2, TD (L1 Physique-Chimie & sciences pour l’ingénieur):
  pointers, multi-dimensional arrays
• Logique, TD (L1 Informatique):
  truth tables, proof by induction, proof systems (NK, LK)
• Programmation fonctionnelle, TP (L2 Informatique):
  OCaml

Past internships

• De la Géométrie de l’Interaction à la Syntaxe Transcendentale (2019/incomplete) with Thomas Seiller. Master 2 informatique (MPRI).
  [report] [slides] [subject]
• Sur l’espace des termes et des machines (2018/incomplete) with Damiano Mazza. Master 1 informatique.
  [report] [slides]
• Etude du langage PCF à travers les réseaux de preuve de la logique linéaire (2017) with Michele Pagani and Delia Kesner. L3 Informatique.
  [report]
• Formalisation des garanties de sécurité apportées par l’isolation de composants logiciels (2016) with Yannis Juglaret. DUT Informatique.
  [report] [slides] [source]