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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,227

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

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.
A short proof of the strong normalization of classical natural deduction with disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
Unification in a A-Calculus with Intersection Types.Michael Kohlhase & Frank Pfenning - unknown
A classification of intersection type systems.M. W. Bunder - 2002 - Journal of Symbolic Logic 67 (1):353-368.
The emptiness problem for intersection types.Paweł Urzyczyn - 1999 - Journal of Symbolic Logic 64 (3):1195-1215.
Strong Normalizability of Typed Lambda-Calculi for Substructural Logics.Motohiko Mouri & Norihiro Kamide - 2008 - Logica Universalis 2 (2):189-207.
Strong normalization for typed terms with surjective pairing.A. S. Troelstra - 1986 - Notre Dame Journal of Formal Logic 27 (4):547-550.
Tarski's fixed-point theorem and lambda calculi with monotone inductive types.Ralph Matthes - 2002 - Synthese 133 (1-2):107 - 129.
Strong Normalization Theorem for a Constructive Arithmetic with Definition by Transfinite Recursion and Bar Induction.Osamu Takaki - 1997 - Notre Dame Journal of Formal Logic 38 (3):350-373.
Various Concepts of “Supervenience” and Their Relations：A Comment on Kim’s Theory of Supervenience.Xiaoping Chen - 2011 - Frontiers of Philosophy in China 6 (2):316-333.
A reduction rule for Peirce formula.Sachio Hirokawa, Yuichi Komori & Izumi Takeuti - 1996 - Studia Logica 56 (3):419 - 426.
Lascar Types and Lascar Automorphisms in Abstract Elementary Classes.Tapani Hyttinen & Meeri Kesälä - 2011 - Notre Dame Journal of Formal Logic 52 (1):39-54.

Analytics

Added to PP
2010-08-24

Downloads
25 (#636,619)

6 months
10 (#276,350)

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.
Functional Characters of Solvable Terms.M. Coppo, M. Dezani-Ciancaglini & B. Venneri - 1981 - Mathematical Logic Quarterly 27 (2‐6):45-58.

Add more references