TypiCal

Intervenant: Alexandre Miquel (ENS Lyon)

Date et lieu: 16/04/2009, 14h Salle de conférence du Lix

Résumé: Mon deuxième exposé (qui fera suite à l'exposé du matin) sera consacré à l'extraction classique dans le cadre de l'assistant à la preuve Coq. Dans un premier temps, je montrerai comment la théorie de la réalisabilité classique de Krivine - définie à l'origine pour l'arithmétique classique du second ordre - peut être étendue au calcul des constructions inductives (pICC) avec tiers-exclu. Ensuite je présenterai le schéma d'extraction classique étendu à pICC ainsi que les diverses optimisations mises en oeuvre dans le module d'extraction classique (notamment en ce qui concerne la représentation des entiers). Enfin, je terminerai mon exposé par quelques exemples de programmes extraits à partir de preuves classiques, sous la forme d'une démo.

Liens: Les transparents de l'exposé.