QuB: A Resource Aware Functional Programming Language

Abstract

Modern programming languages treat resources as normal values. The static semantics of resources in such languages does not match their runtime semantics. In this thesis, we tackle the resource management problem by making resources first class citizens in the language, and concentrating on sharing or separation of resources. We design and implement QuB (pronounced: cube), a Curry-Howard interpretation of logic of bunched implications (BI) (O’Hearn and Pym, 1999). We distinguish two kinds of values—restricted and unrestricted—and two kinds of function implications— sharing and separating. The restricted values model resources while the unrestricted values model program objects that do not contain any resources. Sharing functions denote that functions share resources with its arguments, while separating functions denote that functions do not share resources with its arguments. We show how the use of monads with sharing and separating functions helps in modeling patterns, such as exception handling, that are difficult to express in linear languages.