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

 

Le Jeudi 6 Mai 2010 à 9h45 en Salle 1 - Tour IRMA

 

Séminaire de Mme Dominique DUVAL (PR)

 

Les exceptions sont symétriques des états

 

Résumé:

 

Dans cet exposé je présenterai des travaux en cours concernant la sémantique des langages de programmation, développés avec Laurent Fousse, Jean-Guillaume Dumas et Jean-Claude Reynaud.
Le problème est de trouver un cadre théorique général pour exprimer la sémantique des langages de programmation, quel que soit leur "style". Plus précisément, le but est de prolonger à des langages de styles variés le cadre catégorique qui a été développé dans les années 1970 pour les langages fonctionnels (correspondance de Curry-Howard-Lambek). Pour les langages impératifs, une formalisation catégorique de l'état de la mémoire d'un ordinateur a été proposée par Moggi puis étendue par Plotkin et Power, mais leur méthode s'applique mal au traitement des exceptions. Nous développons une autre approche, dans laquelle le traitement des exceptions peut être vu tout simplement comme symétrique, en un certain sens, de la modification des états. C'est cette symétrie qui sera présentée dans l'exposé, cela donnera l'occasion de (re)voir la symétrie entre le produit et la somme de deux ensembles (c'est-à-dire, le produit cartésien et l'union disjointe).