Résultats de complétude pour des classes de types du système \mathcal {AF}2

DOI10.1051/ITA/1997310605131MaRDI QIDQ4389762zbMATH OpenOpenAlexFDO

Authors Samir Farkh, Karim Nour

Publication date 24 May 1998

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

Full work available at URL https://arxiv.org/abs/0905.0575, https://eudml.org/doc/92576

zbMATH Keywords

\({\mathcal A} {\mathcal F}2\) type system

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Abstract: J.-L. Krivine introduced the AF2 type system in order to obtain programs ($lambda$-terms) which calculate functions, by writing demonstrations of their totalities. We present in this paper two results of completness for some types of AF2 and for many notions of reductions. These results generalize a theorem of R. Labib-Sami established in the system F of J.-Y. Girard.

Recommendations

• Complete types in an extension of the system \({\mathcal A}{\mathcal F}2\)
• Remarks on Semantic Completeness for Proof-Terms with Laird’s Dual Affine/Intuitionistic λ-Calculus
• A filter lambda model and the completeness of type assignment
• scientific article; zbMATH DE number 1555190
• Completeness of type assignment in continuous lambda models

Cites work

• A semantical storage operator theorem for all types
• 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 lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(7)

• The completeness of typing for context-semantics
• Complete types in an extension of the system \({\mathcal A}{\mathcal F}2\)
• scientific article; zbMATH DE number 1555190 (Why is no real title available?)
• Type Decomposition and the Rectangular AFD Property for W*-TRO’s
• scientific article; zbMATH DE number 7204448 (Why is no real title available?)
• A completeness result for the simply typed \(\lambda \mu \)-calculus
• A completeness result for a realisability semantics for an intersection type system

This page was built for publication: Résultats de complétude pour des classes de types du système $\mathcal {AF}2$

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