Forum Numerica - Jorge PÉREZ

lundi 25 mars 2024

Jorge A. Pérez est professeur associé (étudiant) à l'Université de Groningue (Pays-Bas). Depuis 2019, il dirige le Groupe de calcul fondamental, l'une des unités de recherche de l'Institut de mathématiques, d'informatique et d'intelligence artificielle de Bernoulli (www.rug.nl/fse/fc). Le groupe se compose actuellement de cinq membres du personnel de recherche et de 6 doctorants. Il est membre choisi de la Young Academy Groningue. Avant son poste actuel, Jorge A. Pérez a travaillé en tant que chercheur post-doctorant à l'Université NOVA de Lisbonne (Portugal) et a obtenu son doctorat à l'Université de Bologne (Italie). Ses intérêts de recherche concernent la théorie de la concordance, la sémantique des langages de programmation et la logique en informatique. Il a obtenu trois doctorats et en supervise actuellement trois autres. En février 2019-janvier 2024, ses recherches ont été soutenues par le Conseil néerlandais de la recherche (NWO) au titre d'une prestigieuse subvention VIDI intitulée « Unifying correct for Communicating Software ». https://www.jperez.nl/

Résumé :

Dans cette conférence, je parle des travaux récents visant à relever le défi consistant à garantir la propriété de la liberté d'impasse pour les processus de transmission de messages qui communiquent asynchronement dans les réseaux de processus cycliques. Je présenterai deux contributions. Tout d'abord, je présenterai les processus classiques asynchrones basés sur les priorités (APCP), un cadre de processus de type session qui prend en charge la communication asynchrone, la délégation et la récurrence dans les réseaux de processus cycliques. S'appuyant sur les correspondances Curry-Howard entre la logique linéaire et les types de session, l'APCP jouit de propriétés essentielles, notamment de la liberté d'impasse. Deuxièmement, je présenterai et illustrerai un nouveau calcul parallèle avec des types de sessions asynchrones, surnommée LASTon. Je vais illustrer une connexion technique précise entre APCP et LASTin, à savoir comment transférer de manière saine la garantie de liberté d'impasse d'APCP à LASTin.