David Clarke, Sophia Drossopoulou
Ownership types provide a statically enforceable notion of object-level encapsulation. We extend ownership types with computational effects to support reasoning about object-oriented programs. The ensuing system provides both access control and effects reporting. Based on this types system, we codify two formal systems for reasoning ebout aliasing and the disjointness of computational effects. The first can be used to prove that evaluation of two expressions will never lead to aliases, while the latter can be used to show the non-interference of two expressions.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.