Academic Journals Database
Disseminating quality controlled scientific knowledge

Intersection Type Systems and Logics Related to the Meyer-Routley System B+

Author(s): Martin Bunder

Journal: Australasian Journal of Logic
ISSN 1448-5052

Volume: 1;
Start page: 43;
Date: 2003;
VIEW PDF   PDF DOWNLOAD PDF   Download PDF Original page

Keywords: Lambda Calculus | Type Systems | Relevant Logic

Some, but not all, closed terms of the lambda calculus have types; these types are exactly the theorems of intuitionistic implicational logic. An extension of these simple (?) types to intersection (or ??) types allows all closed lambda terms to have types. The corresponding ?? logic, related to the Meyer-Routley minimal logic B+ (without ?), is weaker than the ?? fragment of intuitionistic logic. In this paper we provide an introduction to the above work and also determine the ?? logics that correspond to certain interesting subsystems of the full ?? type theory.
Affiliate Program      Why do you need a reservation system?