Réalisabilité classique Une introduction

icon

73

pages

icon

Français

icon

Documents

2011

Écrit par

Publié par

Lire un extrait
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
icon

73

pages

icon

Français

icon

Ebook

2011

Lire un extrait
Lire un extrait

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

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 icon arrow

Publié par

Publié le

01 mars 2011

Nombre de lectures

35

Langue

Français

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
NGriffin, 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
:::
Griffin, 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
:::
Griffin, 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

Voir icon more
Alternate Text