Un Résultat de Complétude pour les Types ∀ +
Résumé. Nous présentons dans cette note un résultat de complétude pour les types à quantificateurs positifs du système F de J.-Y. Girard. Ce résultat généralise un théorème de R. Labib-Sami (voir [3]). A Completeness Result for the ∀ + Types of System F Abstract. We presente in this note a completen...
Main Author: | |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Published: |
|
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.251.490 http://arxiv.org/pdf/0905.0592v1.pdf |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.251.490 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.251.490 2023-05-15T18:11:23+02:00 Un Résultat de Complétude pour les Types ∀ + Du Système F The Pennsylvania State University CiteSeerX Archives 905 application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.251.490 http://arxiv.org/pdf/0905.0592v1.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.251.490 http://arxiv.org/pdf/0905.0592v1.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://arxiv.org/pdf/0905.0592v1.pdf text ftciteseerx 2016-01-07T19:46:06Z Résumé. Nous présentons dans cette note un résultat de complétude pour les types à quantificateurs positifs du système F de J.-Y. Girard. Ce résultat généralise un théorème de R. Labib-Sami (voir [3]). A Completeness Result for the ∀ + Types of System F Abstract. We presente in this note a completeness result for the types with positive quantifiers of the J.-Y. Girard type system F. This result generalizes a theorem of R. Labib-Sami (see [3]). Abridged English Version. The F type system have been introduced by J.-Y. Girard (see [1]). This system is based on the second order intuitionistic propositional calculus, and thus it gives the possibility to quantify on types. In addition to strong normalisation theorem which certifies the termination of programs, the system F has two more properties: It allows to write programs for all the fonctions whose termination can be proved in the Peano’s second order arithmetics.- It allows to define all the usual data types: booleans, integers, lists, etc. Text sami Unknown |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
ftciteseerx |
language |
English |
description |
Résumé. Nous présentons dans cette note un résultat de complétude pour les types à quantificateurs positifs du système F de J.-Y. Girard. Ce résultat généralise un théorème de R. Labib-Sami (voir [3]). A Completeness Result for the ∀ + Types of System F Abstract. We presente in this note a completeness result for the types with positive quantifiers of the J.-Y. Girard type system F. This result generalizes a theorem of R. Labib-Sami (see [3]). Abridged English Version. The F type system have been introduced by J.-Y. Girard (see [1]). This system is based on the second order intuitionistic propositional calculus, and thus it gives the possibility to quantify on types. In addition to strong normalisation theorem which certifies the termination of programs, the system F has two more properties: It allows to write programs for all the fonctions whose termination can be proved in the Peano’s second order arithmetics.- It allows to define all the usual data types: booleans, integers, lists, etc. |
author2 |
The Pennsylvania State University CiteSeerX Archives |
format |
Text |
author |
Du Système F |
spellingShingle |
Du Système F Un Résultat de Complétude pour les Types ∀ + |
author_facet |
Du Système F |
author_sort |
Du Système F |
title |
Un Résultat de Complétude pour les Types ∀ + |
title_short |
Un Résultat de Complétude pour les Types ∀ + |
title_full |
Un Résultat de Complétude pour les Types ∀ + |
title_fullStr |
Un Résultat de Complétude pour les Types ∀ + |
title_full_unstemmed |
Un Résultat de Complétude pour les Types ∀ + |
title_sort |
un résultat de complétude pour les types ∀ + |
publishDate |
|
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.251.490 http://arxiv.org/pdf/0905.0592v1.pdf |
genre |
sami |
genre_facet |
sami |
op_source |
http://arxiv.org/pdf/0905.0592v1.pdf |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.251.490 http://arxiv.org/pdf/0905.0592v1.pdf |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766184051077545984 |