Les types de données syntaxiques du système ℱ

Samir Farkh; Karim Nour

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2001)

  • Volume: 35, Issue: 3, page 207-221
  • ISSN: 0988-3754

Abstract

top
We give in this paper a purely syntactical definition of input and output types of system ℱ . We define the syntactical data types as input and output types. We show that any type with positive quantifiers is a syntactical data type and that an input type is an output type. We give some restrictions on the ∀ -elimination rule in order to prove that an output type is an input type.

How to cite

top

Farkh, Samir, and Nour, Karim. "Les types de données syntaxiques du système ${\mathcal {F}}$." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 35.3 (2001): 207-221. <http://eudml.org/doc/92662>.

@article{Farkh2001,
abstract = {Nous présentons dans ce papier une définition purement syntaxique des types entrées et des types sorties du système $\{\mathcal \{F\}\}$. Nous définissons les types de données syntaxiques comme étant des types entrées et sorties. Nous démontrons que les types à quantificateurs positifs sont des types de données syntaxiques et qu’un type entrée est un type sortie. Nous imposons des restrictions sur la règle d’élimination des quantificateurs pour démontrer qu’un type sortie est un type entrée.},
author = {Farkh, Samir, Nour, Karim},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {input type; output type; data type; system $\{\mathcal \{F\}\}$; lambda calculus; system ; syntactical definition of input and output types; syntactical data types},
language = {fre},
number = {3},
pages = {207-221},
publisher = {EDP-Sciences},
title = {Les types de données syntaxiques du système $\{\mathcal \{F\}\}$},
url = {http://eudml.org/doc/92662},
volume = {35},
year = {2001},
}

TY - JOUR
AU - Farkh, Samir
AU - Nour, Karim
TI - Les types de données syntaxiques du système ${\mathcal {F}}$
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2001
PB - EDP-Sciences
VL - 35
IS - 3
SP - 207
EP - 221
AB - Nous présentons dans ce papier une définition purement syntaxique des types entrées et des types sorties du système ${\mathcal {F}}$. Nous définissons les types de données syntaxiques comme étant des types entrées et sorties. Nous démontrons que les types à quantificateurs positifs sont des types de données syntaxiques et qu’un type entrée est un type sortie. Nous imposons des restrictions sur la règle d’élimination des quantificateurs pour démontrer qu’un type sortie est un type entrée.
LA - fre
KW - input type; output type; data type; system ${\mathcal {F}}$; lambda calculus; system ; syntactical definition of input and output types; syntactical data types
UR - http://eudml.org/doc/92662
ER -

References

top
  1. [1] S. Farkh, Types de données en logique du second ordre, Thèse de doctorat. Université de Savoie, France (1998). 
  2. [2] S. Farkh et K. Nour, Résultats de complétudes pour les types ∀ + du système ℱ . C. R. Acad. Sci. Paris Sér. I Math. 326 (1998) 275-279. Zbl0908.03032MR1648500
  3. [3] J.-Y. Girard, Y. Lafont et P. Taylor, Proofs and Types. Cambridge University Press (1986). Zbl0671.68002MR1003608
  4. [4] J.-L. Krivine, Lambda-calcul, types et modèles. Masson, Paris (1990). Zbl0697.03004MR1162977
  5. [5] J.-L. Krivine, Classical Logic, Storage Operators and Second Order Lambda-Calculs. Ann. Pure Appl. Logic 68 (1994) 53-78. Zbl0814.03009MR1278549
  6. [6] J.-L. Krivine, Opérateurs de mise en mémoire et traduction de Gödel. Arch. Math. Logic 30 (1990) 241-267. Zbl0712.03009MR1080590
  7. [7] K. Nour, Opérateurs de mise en mémoire en lambda-calcul pur et typé, Thèse de doctorat. Université de Savoie, France (1993). 
  8. [8] K. Nour, Opérateurs de mise en mémoire et types ∀ -positifs. RAIRO : Theoret. Informatics Appl. 30 (1996) 261-293. Zbl0869.03009MR1415831
  9. [9] K. Nour, Les I -types du système ℱ . RAIRO : Theoret. Informatics Appl. (to appear). MR1869215

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.