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

Résumé

Ce cours complète le précédent en terminant la présentation des méthodes générales de preuve de programmes par celle fondée sur les logiques d’ordre supérieur (celles où l’on peut aussi quantifier sur les prédicats) et sur le lambda-calcul déjà présenté en détail dans le cours 2009-2010. Nous montrons d’abord pourquoi l’ordre supérieur est plus expressif que l’ordre un. Par exemple, pour prouver une propriété par récurrence, il faut avoir en calcul des prédicats un schéma d’axiome de récurrence qui engendre un axiome particulier par prédicat à étudier, et donc une infinité d’axiomes ; en ordre supérieur, un seul axiome standard suffit puisqu’on peut quantifier universellement le prédicat de travail. D’autres avantages apparaîtront dans la suite du cours. Un inconvénient est bien sûr une plus grande complexité de la logique et de certains des algorithmes permettant de la traiter.