| dc.contributor.author | Ferreira, Fernando | |
| dc.contributor.author | Ferreira, Gilda | |
| dc.date.accessioned | 2016-12-08T12:03:15Z | |
| dc.date.available | 2016-12-08T12:03:15Z | |
| dc.date.issued | 2016 | |
| dc.identifier.issn | 0138-0680 | |
| dc.identifier.uri | http://hdl.handle.net/11089/20145 | |
| dc.description | 2010 Mathematics Subject Classification. 03F07, 03B20, 03B40 | pl_PL |
| dc.description.abstract | We give an elementary proof (in the sense that it is formalizable in Peano arithmetic)
of the strong normalization of the atomic polymorphic calculus F_{at} (a
predicative restriction of Girard’s system F). | pl_PL |
| dc.description.sponsorship | Both authors acknowledge the support of Fundação para a Ciência e a Tecnologia [UID/MAT/04561/2013] and Centro de Matemática, Aplicações Fundamentais e Investigação Operacional of Universidade de Lisboa. The second author is also grateful to Fundação para a Ciência e a Tecnologia [UID/CEC/00408/2013 and grant SFRH/BPD/93278/2013], to LargeScale Informatics Systems Laboratory (Universidade de Lisboa) and to Núcleo de Investigação em Matemática (Universidade Lusófona). | pl_PL |
| dc.language.iso | en | pl_PL |
| dc.publisher | Uniwersytet Łódzki. Katedra Logiki i Metodologii Nauk | pl_PL |
| dc.relation.ispartofseries | Uniwersytet Łódzki. Katedra Logiki i Metodologii Nauk;45 | |
| dc.subject | predicative polymorphism | pl_PL |
| dc.subject | strong normalization | pl_PL |
| dc.subject | elementary proofs | pl_PL |
| dc.subject | lambda-calculus | pl_PL |
| dc.title | An Elementary Proof of Strong Normalization for Atomic F | pl_PL |
| dc.type | Article | pl_PL |
| dc.page.number | 1-16 | pl_PL |
| dc.contributor.authorAffiliation | Universidade de Lisboa | pl_PL |
| dc.contributor.authorAffiliation | Universidade Lus´ofona de Humanidades e Tecnologias | pl_PL |
| dc.identifier.eissn | 2449-836X | |
| dc.references | T. Altenkirch and T. Coquand, A finitary subsystem of the polymorphic λ- calculus, Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications (TLCA 2001), Lecture Notes in Computer Science 2044 (2001), pp. 22–28. | pl_PL |
| dc.references | A. Beckmann, Exact bounds for lenghts of reductions in typed λ-calculus, The Journal of Symbolic Logic 66(3) (2001), pp. 1277–1285. | pl_PL |
| dc.references | F. Ferreira, A simple proof of Parsons’ theorem, Notre Dame Journal of Formal Logic 46 (2005), pp. 83–91. | pl_PL |
| dc.references | F. Ferreira, Comments on predicative logic, Journal of Philosophical Logic 35 (2006), pp. 1–8. | pl_PL |
| dc.references | F. Ferreira and G. Ferreira, Atomic polymorphism, The Journal of Symbolic Logic 78 (2013), pp. 260–274. | pl_PL |
| dc.references | F. Ferreira and G. Ferreira, The faithfulness of Fat: a proof-theoretic proof, Studia Logica 103(6) (2015), pp. 1303–1311. | pl_PL |
| dc.references | J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and Types, Cambridge University Press (1989). | pl_PL |
| dc.references | F. Joachimski and R. Matthes, Short proofs of normalization for the simplytyped lambda-calculus, permutative conversions and G¨odel’s T, Archive for Mathematical Logic 42 (2003), pp. 59–87. | pl_PL |
| dc.references | H. Schwichtenberg, An upper bound for reduction sequences in the typed λ- calculus, Archive for Mathematical Logic 30 (1991), pp. 405–408. | pl_PL |
| dc.references | W. Tait, Intentional interpretations of functionals of finite type I, The Journal of Symbolic Logic 32 (1967), pp. 198–212. | pl_PL |
| dc.references | W. Tait, Finitism, Journal of Philosophy 78 (1981), pp. 524–546. | pl_PL |
| dc.references | A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Cambridge University Press (1996). | pl_PL |
| dc.references | A. S. Troelstra and D. van Dalen, Constructivism in Mathematics. An Introduction, volume 1, North Holland, Amsterdam (1988). | pl_PL |
| dc.references | J. van de Pol, Two different strong normalization proofs? Computability versus functionals of finite type, Proceedings of the Second International Workshop on Higher-Order Algebra, Logic and Term Rewriting (HOA’95), Lecture Notes in Computer Science 1074 (1996), pp. 201–220. | pl_PL |
| dc.references | F. van Raamsdonk and P. Severi, On normalization, Technical report CSR9545, Centrum voor Wiskunde en Informatica, Amsterdam (1995). | pl_PL |
| dc.contributor.authorEmail | gmferreira@fc.ul.pt | pl_PL |
| dc.identifier.doi | 10.18778/0138-0680.45.1.01 | |
| dc.relation.volume | 1 | pl_PL |
