Complete types in an extension of the system A F2

DOI10.3166/JANCL.13.73-85MaRDI QIDQ3647204zbMATH OpenOpenAlexFDO

Authors Samir Farkh, Karim Nour

Publication date 30 November 2009

Published in Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0905.0371

zbMATH Keywords

typed lambda-calculuscomplete typesecond-order functional arithmeticsystem \({\mathcal A}{\mathcal F}2\)type with positive quantifier

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Abstract: In this paper, we extend the system AF2 in order to have the subject reduction for the $$-reduction. We prove that the types with positive quantifiers are complete for models that are stable by weak-head expansion.

Recommendations

• Résultats de complétude pour des classes de types du système $\mathcal {AF}2$
• βη-complete models for System F
• Subtyping + extensionality: confluence of \(\beta \eta\)top reduction in \(\mathrm{F}_\leq\)
• A note on subject reduction in \((\to, \exists)\)-Curry with respect to complete developments
• scientific article; zbMATH DE number 1555190

Cites work

• A semantical storage operator theorem for all types
• Automatic synthesis of typed -programs on term algebras
• Classical logic, storage operators and second-order lambda-calculus
• Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
• Polymorphic type inference and containment
• Résultats de complétude pour des classes de types du système $\mathcal {AF}2$
• Storage Operators and ∀‐positive Types in TTR Type System
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(5)

• scientific article; zbMATH DE number 1916704 (Why is no real title available?)
• Résultats de complétude pour des classes de types du système $\mathcal {AF}2$
• A note on subject reduction in \((\to, \exists)\)-Curry with respect to complete developments
• scientific article; zbMATH DE number 1555190 (Why is no real title available?)
• scientific article; zbMATH DE number 517016 (Why is no real title available?)

This page was built for publication: Complete types in an extension of the system \({\mathcal A}{\mathcal F}2\)

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