| The Minimal Relevant Logic and the Call-by-Value Lambda Calculus (1999) | |||||||||||||||
Abstract | |||||||||||||||
| The minimal relevant logic B+, seen as a type discipline, includes an extension of Curry types known as the intersection type discipline. We will show that the full logic B+ gives a type assignment system which produces a model of Plotkin's call-by-value -calculus. 1 Introduction The logical system B+ arose from Meyer and Routley's investigation on the negation-free entailment logic [12]. In their approach, B+ turns out as the minimal relevant logic, which is complete with respect to a variant of Kripke models, called the positive model structures. Independently, and with quite different aims, an extension of the Curry type assignment system with "intersection" types was introduced in [3] by Coppo and Dezani. The same authors, together with Barendregt, were able to prove in [2] that, provided a suitable axiomatisation of the subtype relation A B, the set of filters over types is a -model. As a consequence, a completeness theorem for the intersection types assignment system was estab... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||