Les types de données syntaxiques du système
RAIRO - Theoretical Informatics and Applications (2010)
- Volume: 35, Issue: 3, page 207-221
- ISSN: 0988-3754
Access Full Article
top
Abstract
topHow to cite
topFarkh, Samir, and Nour, Karim. "Les types de données syntaxiques du système ${\cal F}$." RAIRO - Theoretical Informatics and Applications 35.3 (2010): 207-221. <http://eudml.org/doc/221944>.
@article{Farkh2010,
abstract = {
We give in this paper a purely syntactical definition
of input and output types of system $\{\cal F\}$. 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.
},
author = {Farkh, Samir, Nour, Karim},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Input type; output type; data type; system $\{\cal F\}$.; lambda calculus; system ; syntactical definition of input and output types; syntactical data types},
language = {eng},
month = {3},
number = {3},
pages = {207-221},
publisher = {EDP Sciences},
title = {Les types de données syntaxiques du système $\{\cal F\}$},
url = {http://eudml.org/doc/221944},
volume = {35},
year = {2010},
}
TY - JOUR
AU - Farkh, Samir
AU - Nour, Karim
TI - Les types de données syntaxiques du système ${\cal F}$
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 35
IS - 3
SP - 207
EP - 221
AB -
We give in this paper a purely syntactical definition
of input and output types of system ${\cal F}$. 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.
LA - eng
KW - Input type; output type; data type; system ${\cal F}$.; lambda calculus; system ; syntactical definition of input and output types; syntactical data types
UR - http://eudml.org/doc/221944
ER -
References
top- S. Farkh, Types de données en logique du second ordre, Thèse de doctorat. Université de Savoie, France (1998).
- 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.
- J.-Y. Girard, Y. Lafont et P. Taylor, Proofs and Types. Cambridge University Press (1986).
- J.-L. Krivine, Lambda-calcul, types et modèles. Masson, Paris (1990).
- J.-L. Krivine, Classical Logic, Storage Operators and Second Order Lambda-Calculs. Ann. Pure Appl. Logic68 (1994) 53-78.
- J.-L. Krivine, Opérateurs de mise en mémoire et traduction de Gödel. Arch. Math. Logic30 (1990) 241-267.
- K. Nour, Opérateurs de mise en mémoire en lambda-calcul pur et typé, Thèse de doctorat. Université de Savoie, France (1993).
- K. Nour, Opérateurs de mise en mémoire et types -positifs. RAIRO: Theoret. Informatics Appl.30 (1996) 261-293.
- K. Nour, Les I-types du système . RAIRO: Theoret. Informatics Appl. (to appear).
NotesEmbed ?
topYou 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.