Valentin "Richie" Maestracci

I’m a Phd Student in the LDP (Logic of Programming) Team of Aix-Marseille Université!

My PhD subject is working on Transcendantal Syntax, a continuation of the research program of Geometry of Interaction, which tries to, among other things, 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).

I’m also a frequent 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.