Résumé de séminaire

Résumé :

Je présenterai un calcul dû à Hugo Herbelin qui interprète la logique classique, plus précisément le calcul des séquents classique. Ceci sera fait dans l'esprit de la correspondance de Curry-Howard, qui considère les propositions comme des types, les preuves comme des programmes et les réductions de preuves comme des calculs.

Du point de vue de la conception de langages de programmation, le calcul de Herbelin est simple et naturel. Il est basé sur des capsules appelant-appelé et le résultat d'un calcul a un type qui dépend de l'exécution du « programme » à la manière d'un programme qui lève des exceptions. Ceci est donc une autre présentation (peut-être plus simple !) de la connexion entre la logique classique et la levée d'exceptions. Ensuite je parlerai de la caractérisation des termes fortement normalisables dans ce calcul à l'aide de types avec intersections.

Je ne ferai pas l'hypothèse que le public connaît le calcul des séquents et même quoi que ce soit sur la logique, puisque que je reprendrai tout à partir de zéro.

Références :

Home page : http://www.ens-lyon.fr/~plescann/