Yann Régis-Gianas : CallCC, un coup d’état sur le contrôle (23/03/2016)

Orateur

Yann Régis-Gianas

Titre

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.

Informations

Mercredi 23 mars 2016, 14h-15h30.

LIP6, salle 24-24/405.

Documents