Strong Normalization and Typability with Intersection Types

Notre Dame Journal of Formal Logic 37 (1):44-52 (1996)
  Copy   BIBTEX

Abstract

A simple proof is given of the property that the set of strongly normalizing lambda terms coincides with the set of lambda terms typable in certain intersection type assignment systems

Categories

Keywords

Reprint years

DOI

10.1305/ndjfl/1040067315

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,247

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing.Steffen van Bakel - 2004 - Notre Dame Journal of Formal Logic 45 (1):35-63.
An elementary proof of strong normalization for intersection types.Valentini Silvio - 2001 - Archive for Mathematical Logic 40 (7):475-488.
Intersection types for lambda-terms and combinators and their logics.Martin Bunder - 2002 - Logic Journal of the IGPL 10 (4):357-378.
Term-Space Semantics of Typed Lambda Calculus.Ryo Kashima, Naosuke Matsuda & Takao Yuyama - 2020 - Notre Dame Journal of Formal Logic 61 (4):591-600.
A decidable theory of type assignment.William R. Stirton - 2013 - Archive for Mathematical Logic 52 (5-6):631-658.
Intersection Type Systems and Logics Related to the Meyer–Routley System B+.Martin Bunder - 2003 - Australasian Journal of Logic 1:43-55.
Church-Rosser property and intersection types.George Koletsos & George Stavrinos - 2008 - Australasian Journal of Logic 6:37-54.
The "Relevance" of Intersection and Union Types.Mariangiola Dezani-Ciancaglini, Silvia Ghilezan & Betti Venneri - 1997 - Notre Dame Journal of Formal Logic 38 (2):246-269.
Lambda-calculus terms that reduce to themselves.Bruce Lercher - 1976 - Notre Dame Journal of Formal Logic 17 (2):291-292.
Making the Hyperreal Line Both Saturated and Complete.H. Jerome Keisler & James H. Schmerl - 1991 - Journal of Symbolic Logic 56 (3):1016-1025.

Analytics

Added to PP
2010-08-24

Downloads
30 (#749,901)

6 months
5 (#1,038,502)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Term-Space Semantics of Typed Lambda Calculus.Ryo Kashima, Naosuke Matsuda & Takao Yuyama - 2020 - Notre Dame Journal of Formal Logic 61 (4):591-600.

Add more citations

References found in this work

Intensional interpretations of functionals of finite type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.
Intensional Interpretations of Functionals of Finite Type I.W. W. Tait - 1975 - Journal of Symbolic Logic 40 (4):624-625.
Functional Characters of Solvable Terms.M. Coppo, M. Dezani-Ciancaglini & B. Venneri - 1981 - Mathematical Logic Quarterly 27 (2-6):45-58.

Add more references