| 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 intersection type discipline. We show that the full logic B+ gives a type assignment system which, although unsound with respect to classical-models, is sound and complete with respect to models of Plotkin call-by-value-calculus. | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||