Valentin "Richie" Maestracci

I’m a Post-Doc student under David Baelde and Joseph Lallemand

We are trying to improve Squirrel, a proof assistant for cryptographic protocol, which has the advantage of being interpreted in the “computational model” providing more powerful guarantees than many provers based on the “symbolic model”.

My PhD subject was working on Transcendantal Syntax, under the guidance of Laurent Regnier and Thomas Seiller This is a continuation of the research program of Geometry of Interaction, one of the aim is to reconstruct logic but from computational properties. In particular, these models internalise correctness of proofs in a computational system (think of it as, instead of having a typechecker like in Rocq or Agda, you can write programs that do the typechecking inside the language). One of my hopes, for the distant future, is that it would allow to have programming languages that can have “extensible type system”: you would import new types and their correctness programs as a library and get an even more powerful type system locally). Maybe even a form of “universal logic”?

I’m also a contributor to the Lambda Lab which is a project originated by my friend Rémy Cerda to try and make something akin to the nlab for the Curry-Howard-Lambek correspondence where I operate under an obscure pseudonym.