Complete types in an extension of the system A F2
From MaRDI portal
Publication:3647204
DOI10.3166/JANCL.13.73-85zbMATH Open1185.03011arXiv0905.0371OpenAlexW1965619950MaRDI QIDQ3647204FDOQ3647204
Authors: Samir Farkh, Karim Nour 
Publication date: 30 November 2009
Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/0905.0371
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
typed lambda-calculuscomplete typesecond-order functional arithmeticsystem \({\mathcal A}{\mathcal F}2\)type with positive quantifier
Cites Work
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
- Polymorphic type inference and containment
- Classical logic, storage operators and second-order lambda-calculus
- Automatic synthesis of typed \(\Lambda\)-programs on term algebras
- Résultats de complétude pour des classes de types du système $\mathcal {AF}2$
- A semantical storage operator theorem for all types
- Storage Operators and ∀‐positive Types in TTR Type System
Cited In (3)
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)
