Title
Intersection types for lambda-terms and combinators and their logics
Abstract
It is well known that the simple types of closed lambda terms or combinators can be interpreted as the theorems of intuitionistic implicational logic (H→). Venneri, using an equivalence between the intersection type system for lambda calculus, without the universal type ω, TA∧λ, and a similar system for combinators, TA∧, shows that the types of TA∧λ are the theorems of a Hilbert-style sublogic of ...
Year
DOI
Venue
2002
10.1093/jigpal/10.4.357
Logic Journal of the IGPL
Field
DocType
Volume
Discrete mathematics,Combinatory logic,Mathematics,Lambda
Journal
10
Issue
ISSN
Citations 
4
1367-0751
2
PageRank 
References 
Authors
0.40
0
1
Name
Order
Citations
PageRank
Martin W. Bunder16416.78