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

Authors

  • Martin Bunder Department of Mathematics, University of Wollongong

DOI:

https://doi.org/10.26686/ajl.v1i0.1762

Abstract

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. 

Downloads

Download data is not yet available.

Author Biography

Martin Bunder, Department of Mathematics, University of Wollongong

Downloads

Published

2012-09-16