Mathematical Logic Quarterly 39 (1):539-544 (1993)

Abstract
In this paper a proof of the normal form theorem for the closed terms of Girard's system F is given by using a computability method à la Tait. It is worth noting that most of the standard consequences of the normal form theorem can be obtained using this version of the theorem as well. From the proof-theoretical point of view the interest of the proof is that the definition of computable derivation here used does not seem to be well founded. MSC: 03F05, 03B15
Keywords Normal‐form theorem  Typed lambda‐calculus
Categories (categorize this paper)
DOI 10.1002/malq.19930390155
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 58,321
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Proofs and Types.Jean-Yves Girard - 1989 - Cambridge University Press.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Storage Operators and Directed Lambda-Calculus.René David & Karim Nour - 1995 - Journal of Symbolic Logic 60 (4):1054-1086.
The Proofs of $Alpha Rightarrow Alpha$ in $P - W$.Sachio Hirokawa - 1996 - Journal of Symbolic Logic 61 (1):195-211.
A Lambda Proof of the P-W Theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - Journal of Symbolic Logic 65 (4):1841-1849.
Reverse Mathematics of Prime Factorization of Ordinals.Jeffry L. Hirst - 1999 - Archive for Mathematical Logic 38 (3):195-201.
Ultimate Normal Forms for Parallelized Natural Deductions.Neil Tennant - 2002 - Logic Journal of the IGPL 10 (3):299-337.
Uniqueness of Normal Proofs in Implicational Intuitionistic Logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.
The Proofs of Α→Α in P - W.Sachio Hirokawa - 1996 - Journal of Symbolic Logic 61 (1):195-211.
$Lambdamu$-Calculus and Bohm's Theorem.Rene David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
A Normal Form Theorem for Lω 1p, with Applications.Douglas N. Hoover - 1982 - Journal of Symbolic Logic 47 (3):605 - 624.

Analytics

Added to PP index
2013-12-01

Total views
24 ( #437,687 of 2,419,798 )

Recent downloads (6 months)
4 ( #192,075 of 2,419,798 )

How can I increase my downloads?

Downloads

My notes