Réalisabilité classique Une introduction

pages

Français

Documents

2011

Écrit par
Aloïs Brunel

Publié par
profil-urra-2012

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

Français

Ebook

2011

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

profil-urra-2012

Publié le

01 mars 2011

Nombre de lectures

Langue

Français

Réalisabilité classique Une introduction Aloïs Brunel Vérité et Preuves - 11 Mars 2011

logique implicative minimale

correspondance preuves-programmes

arithmétique d'ordre supérieur

bornes sur la complexité des programmes

terminaison des programmes

réalisabilité classique

Voir

Publié par

profil-urra-2012

Publié le

01 mars 2011

Nombre de lectures

Langue

Français

Brunel

Réalisabilité classique
Une introduction
Aloïs Brunel
Vérité et Preuves - 11 Mars 2011Introduction
Sommaire
1 Introduction
2 La réalisabilité classique
3 Modèles et vérité subjective
Réalisabilité classique
2 / 30
NCertains programmes sans être typables sont corrects vis-à-vis
de l’ exécution :
let fonction = fun n =>
if n+1=0 then 16
else true
Le terme fonction a moralement le type Nat) Bool
La correction vis-à-vis du typage assure certaines propriétés :
La terminaison des programmes
Des bornes sur la complexité des programmes (logiques allégées)
:::
Réalisabilité classique
1 / 30
NLa correction vis-à-vis du typage assure certaines propriétés :
La terminaison des programmes
Des bornes sur la complexité des programmes (logiques allégées)
:::
Certains programmes sans être typables sont corrects vis-à-vis
de l’ exécution :
let fonction = fun n =>
if n+1=0 then 16
else true
Le terme fonction a moralement le type Nat) Bool
Réalisabilité classique
1 / 30
NGrifﬁn, 90 : pour l’étendre à la logique classique (tiers exclu ou
formule de Peirce), on a besoin d’une nouvelle instruction : call-cc.
De manière générale, pour habiter de nouveaux axiomes il faut de
nouveaux programmes.
La correspondance preuves-programmes
Logique implicative minimale $ -calcul simplement typé
!Arithmétique d’ordre supérieur $ système F
:::
Réalisabilité classique
2 / 30
NDe manière générale, pour habiter de nouveaux axiomes il faut de
nouveaux programmes.
La correspondance preuves-programmes
Logique implicative minimale $ -calcul simplement typé
!Arithmétique d’ordre supérieur $ système F
:::
Grifﬁn, 90 : pour l’étendre à la logique classique (tiers exclu ou
formule de Peirce), on a besoin d’une nouvelle instruction : call-cc.
Réalisabilité classique
2 / 30
NLa correspondance preuves-programmes
Logique implicative minimale $ -calcul simplement typé
!Arithmétique d’ordre supérieur $ système F
:::
Grifﬁn, 90 : pour l’étendre à la logique classique (tiers exclu ou
formule de Peirce), on a besoin d’une nouvelle instruction : call-cc.
De manière générale, pour habiter de nouveaux axiomes il faut de
nouveaux programmes.
Réalisabilité classique
2 / 30
N