Notre Dame Journal of Formal Logic 61 (4):591-600 (2020)

Barendregt gave a sound semantics of the simple type assignment system λ → by generalizing Tait’s proof of the strong normalization theorem. In this paper, we aim to extend the semantics so that the completeness theorem holds.
Keywords completeness   soundness  typed lambda calculus
Categories (categorize this paper)
DOI 10.1215/00294527-2020-0028
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: 59,687
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

Intensional Interpretations of Functionals of Finite Type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.
Strong Normalization and Typability with Intersection Types.Silvia Ghilezan - 1996 - Notre Dame Journal of Formal Logic 37 (1):44-52.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

A Completeness Result for the Simply Typed Λμ-Calculus.Karim Nour & Khelifa Saber - 2010 - Annals of Pure and Applied Logic 161 (1):109-118.
Ordinals and Ordinal Functions Representable in the Simply Typed Lambda Calculus.N. Danner - 1999 - Annals of Pure and Applied Logic 97 (1-3):179-201.
Recursion Theory and the Lambda-Calculus.Robert E. Byerly - 1982 - Journal of Symbolic Logic 47 (1):67-83.
Typed Logics with States.J. van Eijck - 1997 - Logic Journal of the IGPL 5 (5):623-645.
Kripke-Style Models for Typed Lambda Calculus.John C. Mitchell & Eugenio Moggi - 1991 - Annals of Pure and Applied Logic 51 (1-2):99-124.
Context Update for Lambdas and Vectors.Reinhard Muskens & Mehrnoosh Sadrzadeh - 2016 - In Maxime Amblard, Philippe de Groote, Sylvain Pogodalla & Christian Retoré (eds.), Logical Aspects of Computational Linguistics. Celebrating 20 Years of LACL (1996--2016). Berlin Heidelberg: Springer. pp. 247--254.
Topological Representation of the Lambda-Calculus.Steve Awodey - 2000 - Mathematical Structures in Computer Science 10 (1):81-96.


Added to PP index

Total views
5 ( #1,151,152 of 2,432,280 )

Recent downloads (6 months)
5 ( #138,513 of 2,432,280 )

How can I increase my downloads?


My notes