Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
En libre accès, dans la limite des places disponibles
-

Résumé

Au cours de son exposé, François Pottier a montré qu'une logique de programmes permet non seulement d'établir la correction d'un programme, mais aussi de contrôler le nombre d'opérations qu'il effectue, et donc, indirectement, son temps de calcul.

Il a expliqué comment ce comptage peut se faire d'abord en logique de Hoare, puis en logique de séparation, où le comptage du temps peut s'effectuer de façon plus décentralisée, et où des artifices comptables très élaborés peuvent être mis en place par l'utilisateur.

Intervenants

François Pottier

Inria