“Iknowonething:Iknownothing”

— Socrates

Projects

mini-compiler: From an ML-flavoured Language to x86-64

A C++17 compiler to x86-64 — graph-colouring register allocation, Cheney GC, closures — and what formal verification actually buys in building one.

C++17Lean 4Z3CompilersFormal Verification

God, Substance, and Necessity: Formalizing Spinoza's Ethics in Lean 4

Machine-checked formalization of Spinoza's Ethics Part I using Lean 4 and Mathlib.

Lean4MathlibFormal VerificationPhilosophy

Optimal Texas Hold'em Strategy Laboratory

Texas Hold'em engine with Monte Carlo simulation, formal Lean4 proofs, and RL agents.

PythonLean4Monte CarloReinforcement LearningMachine Learning

Line-Following Robot with micro:bit

A line-following robot using BBC micro:bit, SparkFun MotoBit, and IR sensors with calibration and state-machine control.

MicroPythonmicro:bitRoboticsI2C

3D Drone Digital Twin in Modelica

Full 3D digital twin of a quadrotor drone using OpenModelica and MSL.

ModelicaOpenModelicaControl SystemsSimulation

Glass Cutting Optimization — ROADEF 2018

6th place out of 64 teams in the ROADEF/EURO 2018 industrial optimization challenge by Saint-Gobain.

C++OpenMPGenetic/EvolutionnarySimulated AnnealingHeuristics

CTU-Solver — Constraint & Integer Programming in Rust

A Rust library combining Constraint Programming (CP) and Integer Programming (IP) with 33+ constraint types, AC-3 propagation, and a simplex solver.

RustConstraint ProgrammingInteger ProgrammingOptimization

Acoustic Guitar Physical Simulation

Full acoustic chain: 1D string FEM, 2D Kirchhoff-Love soundboard, 3D Yee grid air radiation with PML.

PythonNumPySciPyGetFEMGmshFEM

Sea Ice Drift Estimation: MCC vs CMCC

Cross-correlation methods for Arctic sea ice drift from satellite imagery, validated against IABP buoy tracks.

RustPythonAMSR2 dataASCAT data

GMT — Generic Maths Tool

Scientific computing library: Gaussian process regression, tension splines, ridge regression, Monte Carlo simulation, and neural networks.

PythonNumPySciPyMachine LearningGP Regression

Space Altimetry and Continental Hydrology

Multi-level satellite altimetry pipeline: Kalman filtering, kriging, waveform retracking, and multi-mission fusion with Dask.

PythonKrigingKalman FilterSARSatellite Altimetry

CVWeb

This portfolio website — a bilingual, animated CV built with Next.js and Tailwind CSS.

Next.jsTypeScript

“WRITINGshowshowsloppyyourTHINKINGis,

MATHSshowshowsloppyyourWRITINGis,

PROGRAMMINGshowshowsloppyyourMATHis.”

— Leslie Lamport