About your gracious host

In short

My whereabouts

Postdoc at the University of Iceland in Reykjavík, working both on combinatorial species in Lean (with Anders Claesson) and hardware verification in Rocq.

My interests

Formal logic and automated proofs, programming languages, hardware and operating systems.

Online profiles

Gitlab
Ludum Dare (as part of the 👑 Ludum Darons 👑 team)
I do CTFs every so often, usually under the name encrypteur_digital (I like OSINT; 1st/218@BIG2025, 2nd/245@THCon2K25)

Trivia

My name is Matthieu Baty.
My email address is <insert_my_gitlab_username>@protonmail.com.

Experience

CentraleSupélec — 2021–2024

Teaching assistant for the compilers and formal methods courses of the INFOSEC degree (cybersecurity).

EPFL, SYSTEMF lab — 2023, six months, PhD project student

Worked on Coq's support for partial interpretation, under the supervision of Clément Pit-Claudel. See my report.

ANSSI — 2020, six months, fifth year internship

Worked with OCaml, POSIX, Coq (and FreeSpec!), survived a global pandemic. Two deliverables:

A structured documentation of the C standard library introduced in the POSIX standard
An extension of the FreeSpec standard library to bring POSIX primitives into Coq

Fridata — 2018, three months, third year internship

Worked on the development of a radio-tracking system for small animals (e.g. bats) with R/Shiny, in Freiburg im Breisgau, Germany.

Education

2021–2024 — CentraleSupélec/Inria (SUSHI team) — PhD

Formal methods and hardware.
Funded and co-supervised by ANSSI (thanks!).

2015–2020 — University of Strasbourg — BSc/MSc in Computer Science

Computer graphics.

Awards and achievements

N/A