Notre Dame Journal of Formal Logic 38 (2):246-269 (1997)
|Abstract||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)|
|Through your library||Configure|
Similar books and articles
Silvia Ghilezan (1996). Strong Normalization and Typability with Intersection Types. Notre Dame Journal of Formal Logic 37 (1):44-52.
M. W. Bunder (2002). A Classification of Intersection Type Systems. Journal of Symbolic Logic 67 (1):353-368.
Pawel Urzyczyn (1999). The Emptiness Problem for Intersection Types. Journal of Symbolic Logic 64 (3):1195-1215.
Beihai Zhou (1999). Grafted Frames and S1-Completeness. Journal of Symbolic Logic 64 (3):1324-1338.
Robert Arp (2004). Plotinus, Mysticism, and Mediation. Religious Studies 40 (2):145 - 163.
Bikash Kumar Bhattacharya (1989). A Union Catalogue of Philosophical Periodicals. Indian Council of Philosophical Research in Association with Munshiram Manoharlal Publishers.
A. R. P. Robert (2004). Plotinus, Mysticism, and Mediation. Religious Studies 40 (2):145-163.
Renling Jin (2007). Inverse Problem for Cuts. Logic and Analysis 1 (1):61-89.
Abou Jeng (2012). Peacebuilding in the African Union: Law, Philosophy and Practice. Cambridge University Press.
Yoko Motohama, Robert K. Meyer & Mariangiola Dezani-Ciancaglini (2002). The Semantics of Entailment Omega. Notre Dame Journal of Formal Logic 43 (3):129-145.
Henk Barendregt, Mario Coppo & Mariangiola Dezani-Ciancaglini (1983). A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic 48 (4):931-940.
Geoffrey Brennan & Daniel Moseley (forthcoming). Economics and Ethics. In Hugh LaFollette (ed.), International Encyclopedia of Ethics. Wiley-Blackwell.
Boško Živaljević (1991). U-Meager Sets When the Cofinality and the Coinitiality of U Are Uncountable. Journal of Symbolic Logic 56 (3):906-914.
Rosaria Burchielli (2006). The Purpose of Trade Union Values: An Analysis of the ACTU1 Statement of Values. [REVIEW] Journal of Business Ethics 68 (2):133 - 142.
Sorry, there are not enough data points to plot this chart.
Added to index2010-08-24
Recent downloads (6 months)0
How can I increase my downloads?