Valentin Robert

Research & Engineering

I enjoy constructing, manipulating, and reasoning about programs algebraically. Unsurprisingly, I am particularly fond of dependent type systems, functional programming, algebraic effects, with a subtle amount of category theory. I particularly enjoy finding practical uses for theoretical results, and think a lot about making programming and theorem proving easier to learn and educate about.

On my free time, you may find me playing story-heavy video games, playing the guitar, biking around Portland, or playing Yu-Gi-Oh!

Background

Valentin worked at Inria on the formally-verified compiler CompCert during his undergraduate studies, where he implemented the first mechanically-verified alias analysis, and worked on checking the assembly and linking process for the PowerPC target architecture. He also authored the French translation of Learn You a Haskell (http://lyah.haskell.fr/). During his PhD at UC San Diego, he developed PeaCoq, a tool to make interactive theorem proving more user-friendly, and Chick, a tool to help in refactoring dependently-typed functional programs.

At Galois, Valentin has been working on automated translation of Cryptol code to Coq, and on a software provenance analysis tool based on the Nix package manager.

Email Valentin Robert

Current Projects