Output details
11 - Computer Science and Informatics
University of Aberdeen
Bunched Polymorphism
<11>This paper reports the first development anywhere of polymorphically typed lambda calculus with sub-structural features at the second-order level. The type theory and its semantics provide a systematic framework for reasoning, in a uniform style, about the features of programming languages such as ML and its derivatives. The underlying theory and its models are closely related to Separation Logic, so opening the possibility of further theoretical integration of programming language semantics and program logic (to handle features such as polymorphic references). The journal in which this paper appears is the leading one for logic applied in programming language semantics.