Syntactical data types of system F

DOI10.1051/ITA:2001117MaRDI QIDQ2773019zbMATH OpenOpenAlexFDO

Authors Samir Farkh, Karim Nour

Publication date 29 April 2002

Published in RAIRO. Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0905.0754, http://www.numdam.org/item?id=ITA_2001__35_3_207_0, https://eudml.org/doc/221944

zbMATH Keywords

lambda calculussyntactical data typessyntactical definition of input and output typessystem \({\mathcal F}\)

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We give in this paper a purely syntactical definition of input and output types of system 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 $forall$-elimination rule in order to prove that an output type is an input type.

Recommendations

• The I-types of system F
• scientific article; zbMATH DE number 417312
• scientific article; zbMATH DE number 761284
• An extension of system \(F\) with subtyping
• The system \({\mathcal F}\) of variable types, fifteen years later

Cites work

• Classical logic, storage operators and second-order lambda-calculus
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 46869 (Why is no real title available?)
• Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
• Opérateurs de mise en mémoire et types \forall -positifs
• The I-types of system F
• Un résultat de complétude pour les types ∀+ du système F

Cited in

(2)

• scientific article; zbMATH DE number 1088047 (Why is no real title available?)
• scientific article; zbMATH DE number 1555190 (Why is no real title available?)

This page was built for publication: Syntactical data types of system \(\mathcal F\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2773019)