Une sémantique catégorique pour le lambda calcul avec constructeurs

English

Séminaire Modèles et Algorithmes Déterministes: CASYS

26/04/2012 - 09:45 Mme Barbara Petit Salle 1 - Tour IRMA

Le lambda calcul est un langage universel pour représenter le calcul de fonctions, et il est à la base de tous les langages de programmation fonctionnels (Lisp, Haskell, ML etc). Malgré sa syntaxe minimale, il permet d'exprimer n'importe quelle fonction calculable grâce à des encodages. Ces encodages peuvent toutefois s'avérer assez lourds, et éloignent le lambda calcul de l'implémentation concrète des langages de programmation.

Il est donc courant d'enrichir sa syntaxe avec constructions primitives telles que les structures de données ou les exceptions. Il devient alors possible d'étudier ces nouvelles  constructions et leur interaction avec le noyau fonctionnel pur des langages de programmation en faisant abstraction de leur implémentation.

Dans cet exposé nous nous intéresserons à une extension du lambda calcul avec des constructeurs et une opération de filtrage de constantes, capable de décomposer le pattern matching à la ML en opérations atomiques. Nous aborderons aussi la question d'une sémantique dénotationnelle pour ce calcul.