Valentin "Richie" Maestracci

Actuellement en Post-Doc sous la super-vision de David Baelde et Joseph Lallemand

Nous essayons d’améliorer les fondements sémantiques de Squirrel, un assistant de preuves pour la cryptographie, qui a l’avantage d’être dans le “modèle computationel” ce qui donne des garanties plus fortes que la plupart des prouveurs, qui sont basés sur les “modèles symboliques”. Notre but actuel est de changer la sémantique de Squirrel en utilisant de la sémantique des jeux, pour faciliter le raisonnement sur les fonctions d’ordre supérieure. On essaye aussi de régler un autre problème: les garanties de Squirrel ne sont pas exactement celles attendues par les cryptographes (un peu plus faible), mais quitte à avoir une nouvelle sémantique, on peut essayer d’y remédier.

J’ai effectué ma thèse avec Laurent Regnier et Thomas Seiller sur de Réalisabilité Linéaire (ou Syntaxe Transcendantale).

C’est une continuation du programme de recherche de la Géometrie de l’Interaction (GoI). Un des buts est de “reconstuire” la logique (justifier pourquoi la logique est logique), en partant de ses propriétés calculatoires.

On crée des modèles de calculs qui internalise la correction des preuves: certains programmes correspondent à des tests (danos-regnier, long-chemin etc…), ce qui permet d’obtenir des résultats de complétude forte.

Vous poubez y penser comme des langages dont les type-checker sont eux même des programmes du langage (a opposer a des type-checker externe comme Rocq ou Agda)

Un de mes espoirs pour un futur lointain serait d’avoir des langages de programmation avec système de type extensible: on importerait des nouveaux types comme des librairies, ce qui permettrait d’imposer aux programmes des comportements de plus en plus restreints selon les besoins. Peut-être que ce genre de point de vue permettrait même de créer une Logique Universelle”, mais c’est très spéculatif…

Il m’arrive parfois de contribuer au Lambda Lab, un projet super initié par mon ami Rémy Cerda, qui voulait créer une forme de nlab pour la correspondance de Curry-Howard-Lambek. J’y opère en effet sous un obscur pseudonyme.