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.
The University of Kansas prohibits discrimination on the basis of race, color, ethnicity, religion, sex, national origin, age, ancestry, disability, status as a veteran, sexual orientation, marital status, parental status, gender identity, gender expression and genetic information in the University’s programs and activities. The following person has been designated to handle inquiries regarding the non-discrimination policies: Director of the Office of Institutional Opportunity and Access, IOA@ku.edu, 1246 W. Campus Road, Room 153A, Lawrence, KS, 66045, (785)864-6414, 711 TTY.