Accueil
Introduction
Le groupe Géométrie du calcul vise à trouver au sein de la logique et des mathématiques des outils permettant la modélisation abstraite des programmes. Un exemple spectaculaire du succès de cette approche est l'invention de la logique linéaire issue d'une part de l'isomorphisme de Curry-Howard établissant la correspondance entre les déductions formelles en logique intuitionniste et le lambda-calcul typé, et d'autre part de la modélisation du lambda-calcul par des espaces présentant des analogies fortes avec les espaces vectoriels.
Dans ce cadre général le groupe poursuivra notamment mais non exclusivement les objectifs suivants :
- poursuivre les travaux sur la correspondance preuve/programme, avec deux sous-objectifs majeurs : étudier les sémantiques de réalisabilité qui posent le problème profond de comprendre le sens opérationnel des énoncés mathématiques, et étendre les systèmes logiques de typage à des langage plus expressifs que le simple lambda-calcul, typiquement les calculs parallèles ;
- poursuivre les travaux en complexité implicite visant à représenter des classes de complexité algorithmique par des contraintes logiques (logique linéaire légère, Bellantoni-Cook);
- développer le cadre topologique pour la concurrence et la géométrie de la réécriture dans la lignée des travaux sur l'homotopie dirigée qui fournissent un cadre très élégant pour raisonner sur les problèmes de synchronisation entre processus;
- explorer certaines pistes particulièrement prometteuses et récemment apparues donnant à penser qu'une unification conceptuelle est possible entre les paradigmes de calcul séquentiel (lambda-calcul) et parallèle (pi-calcul) : citons en particulier les rapprochements entre la sémantique des jeux et les systèmes de transitions vus comme jeux positionnels, et les analogies entre le lambda-calcul différentiel et le calcul avec ressources.
L'inscription est obligatoire pour bénéficier des pauses café, mais l'accès aux exposés est libre.
Cours
La rencontre s'articule autour de deux cours de 5h chacun, plus deux exposés invités.
Techniques « up-to » et applications en algorithmique
Par Damien Pous (ENS Lyon).
Damien présentera ses travaux récents sur les bisimulations « up to » en la théorie de la concurrence et leurs applications en algorithmique.
New Trends in Parametricity
By Neil Ghani (Strathclyde, Royaume-Uni).
What is Parametricity? Many have heard of it but, for such a fundamental concept, more people ought to understand more about it. Parametricity, also known as logical relations, is a fundamental concept within programming languages designed to capture the idea that programs map related inputs to related outputs. Originally formulated by John Reynolds in the 1970s, parametricity has been a key tool in reasoning about programming languages ever since. However, recent work is beginning to suggest that parametricity is a much deeper concept with potential applications across mathematics, physics and other areas.
In these talks, I'll explain some work we have been doing in Strathclyde which follows Hermida's fibrational approach in suggesting that while the usual semantics of programming languages can be given abstractly in terms of a categorical universe using concepts such as categories, functors and natural transformations, parametricity amounts to working in a fibrational universe consisting of fibred categories, fibred functors and fibred natural transformations. We will start with basic models of System F, consider recent work on parametricity and Martin-Lof Type theory and then move to higher dimensional parametricity and speculate on connections with Homotopy Type Theory.
Exposés invités
Denotational semantics from domains to quantitative semantics
By Thomas Ehrhard (PPS).
Monoidal Turing Categories
By Robin Cockett (Calgary, Canada).
(Turing categories are an axiomatic approach to models of computations, including computability, complexity, and realisability.)
Exposés contribués
Les participants sont aussi invités à proposer des exposés.
Programme
Le programme devrait se remplir, ici.
