CallCC, un coup d’état sur le contrôle (Yann Régis-Gianas)

Pour la prochaine séance du séminaire « Codes sources », nous aurons l’honneur de recevoir Yann Régis-Gianas le mercredi 23 mars 2016, de 14h-16h, au LIP6. Vous trouverez ci-dessous davantage de détails sur ce séminaire.

L’exposé est intitulé : « CallCC, un coup d’état sur le contrôle ».

Résumé :

Lorsque Dijkstra publie son article “Go To Statement Considered Harmful”, une fronde de programmeurs - dont Knuth - s’est élevée contre les restrictions d’expressivité proposées par l’informaticien néerlandais : en effet, la structuration du flot de contrôle par les seules procédures et boucles while interdisait certains idiomes de programmation fort utiles et répandus.

Cependant, les motivations de Dijkstra étaient légitimes : puisque l’on ne peut pas prédire les prédécesseurs d’un point de contrôle en présence du “goto”, on ne peut pas raisonner localement sur les instructions d’un programme et cela interdit toute ambition de passage à l’échelle de la preuve de programme.

Seulement, l’expressivité du “goto” peut être retrouvée à l’aide d’opérateurs de contrôle inventés par Peter Landin plusieurs années auparavant : en présence de ces opérateurs, les points de contrôle deviennent des objets de première classe appelés continuations. En tant qu’objet du calcul, les points de contrôle du programme sont alors l’affaire du programmeur. Grâce à l’abstraction de type, il peut alors choisir de légiférer comme bon lui semble pour spécifier leur bon usage.

Lieu :

Salle 24-25/405 du LIP6 (rotonde 24 ou 25, 4e étage)

Adresse :

4 place Jussieu, 75005 Paris métro Jussieu (lignes 7 et 10)