Zacharie Moughanim
Contact
zacharie [dot] moughanim [at] ens-rennes [dot] fr
zacharie [dot] moughanim [at] ens-rennes [dot] fr
Symbolic bideduction problem (report) Intenship in the SPICY team in Rennes during summer 2026, supervised by Stéphanie Delaune and David Baelde. Study of the (un)decidability of the bideduction problem in the symbolic cryptographic model within different settings.
Cryptographic proofs in Approxis (report) (slides) (contribution) Internship at LOGSEM group, Århus University in Århus, Denmark, supervised by Lars Birkedal and Philipp G. Haselwarter. Cryptographic proofs in the relational separation logic Approxis (formalized within the Rocq framework Iris).
Secrecy by typing in the computational model (report) Research project during the school year 2024/2025 in the SPICY team, supervised by Stéphanie Delaune, Clément Hérouard and Joseph Lallemand. Extended a previous work on security guarantee obtained from a type system.
The weak algebraic λ-calculus (paper) (slides) An accepted paper for the conference Journées Françaises des Langages Applicatifs (JFLA), resulting from my 2024 Internship, supervised by Lionel Vaux Auclair.
TresMLA functional language to produce server-side evaluated, dynamic webpages.
VSquirrel & PySquirrel Prover LSP A VSCode/VSCodium extension for the Squirrel proof assistant, relying on the PySquirrel Prover LSP, a LSP server for Squirrel written in Python.
λMLCompiler2A project of verified compiler (in Coq/Rocq) from a subset of OCaml towards untyped λ-calculus, using Scott encoding.
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.