Complete Types in an Extension of the System AF2
作者： Samir Farkh , Karim Nour
关键词:
摘要: In this paper, we extend the system AF2 in order to have subject reduction for s?-reduction. We prove that types with positive quantifiers are complete models stable by wea...
harvard.edu
philpapers.org
sci-hub.se 参考文章(8)
Corrado Böhm, Alessandro Berarducci, Automatic synthesis of typed Λ-programs on term algebras☆ Theoretical Computer Science. ,vol. 39, pp. 135- 154 ,(1985) , 10.1016/0304-3975(85)90135-5
Samir Farkh, Karim Nour, Résultats de complétude pour des classes de types du système $\mathcal {AF}2$ Theoretical Informatics and Applications. ,vol. 31, pp. 513- 537 ,(1997) , 10.1051/ITA/1997310605131
Karim Nour, Storage Operators and ∀-positive Types in TTR Type System Mathematical Logic Quarterly. ,vol. 42, pp. 349- 368 ,(1996) , 10.1002/MALQ.19960420130
Jean-Louis Krivine, Opérateurs de mise en mémoire et traduction de Gödel Archive for Mathematical Logic. ,vol. 30, pp. 241- 267 ,(1990) , 10.1007/BF01792986
Jean-Louis Krivine, Classical logic, storage operators and second-order lambda-calculus Annals of Pure and Applied Logic. ,vol. 68, pp. 53- 78 ,(1994) , 10.1016/0168-0072(94)90047-7
Christophe Raffalli, A semantical storage operator theorem for all types Annals of Pure and Applied Logic. ,vol. 91, pp. 17- 31 ,(1998) , 10.1016/S0168-0072(97)00041-9
John C. Mitchell, Polymorphic type inference and containment Information & Computation. ,vol. 76, pp. 153- 193 ,(1988) , 10.1016/0890-5401(88)90009-0
Henk Barendregt, The Lambda Calculus. Its Syntax and Semantics ,(2012)