Uniqueness Typing For A Higher-Order Language

Authors: Adrian Francalanza, Melanie Zammit

Corresponding: Adrian Francalanza (adrian.francalanza@um.edu.mt)

Keywords: none

Doi: http://dx.medra.org/10.7423/XJENZA.2014.2.03

Issue: Xjenza Online Vol. 2 Iss. 2 - October 2014

Abstract:
We investigate type-based analysis for a higher-order channel passing language with strong update, whereby messages of a different kind are communicated over the same channel. In order to reason about such pro- grams, our type system employs the concept of uniqueness to be able to assert when it is safe to change the object type a channel. We design a type system based on this concept and prove that our type system is sound, meaning that it only accepts programs that do not produce runtime errors.

Download Article: