Intersection Types as Logical Formulae
- 1 April 1994
- journal article
- research article
- Published by Oxford University Press (OUP) in Journal of Logic and Computation
- Vol. 4 (2) , 109-124
- https://doi.org/10.1093/logcom/4.2.109
Abstract
The aim of this paper is to investigate, in the Curry-Howard isomorphism approach, a logical characterization for the intersection-type discipline. First a novel formulation of the intersection type inference for combinatory logic is presented, such that it is equivalent to the original version of the system, while the intersection operator is no longer dealt with as a proof-theoretical connective. Then a Hilbert-style axiomatization is defined and proved to totally parallel intersection-derivability, in such a way that inhabited intersection-types are all and only the provable formulae in the logic system.Keywords
This publication has 0 references indexed in Scilit: