Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing

Notre Dame Journal of Formal Logic 45 (1):35-63 (2004)
  Copy   BIBTEX

Abstract

This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types

Categories

Keywords

Reprint years

DOI

10.1305/ndjfl/1094155278

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,296

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

Strong Normalization and Typability with Intersection Types.Silvia Ghilezan - 1996 - Notre Dame Journal of Formal Logic 37 (1):44-52.
An elementary proof of strong normalization for intersection types.Valentini Silvio - 2001 - Archive for Mathematical Logic 40 (7):475-488.
A normalizing system of natural deduction for intuitionistic linear logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
Intersection types for lambda-terms and combinators and their logics.Martin Bunder - 2002 - Logic Journal of the IGPL 10 (4):357-378.
Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
Call-by-name reduction and cut-elimination in classical logic.Kentaro Kikuchi - 2008 - Annals of Pure and Applied Logic 153 (1-3):38-65.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
A classification of intersection type systems.M. W. Bunder - 2002 - Journal of Symbolic Logic 67 (1):353-368.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
On the role of implication in formal logic.Jonathan P. Seldin - 2000 - Journal of Symbolic Logic 65 (3):1076-1114.

Analytics

Added to PP
2010-08-24

Downloads
14 (#1,020,370)

6 months
35 (#103,417)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

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.
The Semantics of Entailment Omega.Yoko Motohama, Robert K. Meyer & Mariangiola Dezani-Ciancaglini - 2002 - Notre Dame Journal of Formal Logic 43 (3):129-145.
Strong Normalization and Typability with Intersection Types.Silvia Ghilezan - 1996 - Notre Dame Journal of Formal Logic 37 (1):44-52.

Add more references