Un résultat de complétude pour les types ∀ + du système F
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 Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Published: |
1998
|
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.297.4293 http://www.lama.univ-savoie.fr/~nour/CompF.pdf |
| Summary: | 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. The semantics of the system F proposed by J.-Y. Girard and J.-L. Krivine (see |
|---|