Notre Dame Journal of Formal Logic 38 (2):246-269 (1997)
The aim of this paper is to investigate a Curry-Howard interpretation of the intersection and union type inference system for Combinatory Logic. Types are interpreted as formulas of a Hilbert-style logic L, which turns out to be an extension of the intuitionistic logic with respect to provable disjunctive formulas (because of new equivalence relations on formulas), while the implicational-conjunctive fragment of L is still a fragment of intuitionistic logic. Moreover, typable terms are translated in a typed version, so that --typed combinatory logic terms are proved to completely codify the associated logical proofs
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Strong Normalization and Typability with Intersection Types.Silvia Ghilezan - 1996 - Notre Dame Journal of Formal Logic 37 (1):44-52.
A Classification of Intersection Type Systems.M. W. Bunder - 2002 - Journal of Symbolic Logic 67 (1):353-368.
The Emptiness Problem for Intersection Types.Pawel Urzyczyn - 1999 - Journal of Symbolic Logic 64 (3):1195-1215.
A Union Catalogue of Philosophical Periodicals.Bikash Kumar Bhattacharya - 1989 - Indian Council of Philosophical Research in Association with Munshiram Manoharlal Publishers.
Peacebuilding in the African Union: Law, Philosophy and Practice.Abou Jeng - 2012 - Cambridge University Press.
The Semantics of Entailment Omega.Yoko Motohama, Robert K. Meyer & Mariangiola Dezani-Ciancaglini - 2002 - Notre Dame Journal of Formal Logic 43 (3):129-145.
A Filter Lambda Model and the Completeness of Type Assignment.Henk Barendregt, Mario Coppo & Mariangiola Dezani-Ciancaglini - 1983 - Journal of Symbolic Logic 48 (4):931-940.
Added to index2010-08-24
Total downloads19 ( #259,934 of 2,172,599 )
Recent downloads (6 months)1 ( #325,337 of 2,172,599 )
How can I increase my downloads?