29/03/2007
Lionel Vaux (IML)
Un lambda-bar-mu calcul avec produit de convolution sur les piles

On présente une extension du lambda-bar-mu calcul de Herbelin avec une opération binaire sur les piles (ou contextes), qui peut être interprétée comme un opérateur de choix non déterministe. Les règles de réduction dotent cette opération de propriétés similaires à celles du produit de convolution sur les distributions. C'est la version lambda-calculesque d'une extension par polarisation des réseaux d'interaction différentiels d'Ehrhard-Régnier: on met ce fait en évidence grâce à une sémantique dénotationnelle dans la catégorie des ensembles et relations.