Zacharie Moughanim

The weak algebraic λ-calculus

An accepted paper for the conference Journées Françaises des Langages Applicatifs (JFLA), resulting from my 2024 Internship, supervised by Lionel Vaux Auclair.

λMLCompiler2

A project of verified compiler (in Coq/Rocq) from a subset of OCaml towards untyped λ-calculus, using Scott encoding. Apart from the attempt to prove the compiler in Coq, this project differs from λMLCompiler version 1 in that it is implemented in OCaml and not in C.

λMLCompiler

A transpiler project, translating a subset of OCaml towards untyped λ-calculus.

Research project from the TIPE

The Travaux d'Initiatives Personnels encadrés (TIPE) within the french Classes Préparatoires aux Grandes Écoles (CPGE) program lead me to investigate open problems from a paper, and also to add a new sequence to the OEIS.