Please use this identifier to cite or link to this item:
Title: UJ : type soundness for universe types
Other Titles: Formal methods for components and objects
Authors: Cunningham, Dave
Francalanza, Adrian
Drossopoulou, Sophia
Dietl, Werner
Muller, Peter
Keywords: Object-oriented methods (Computer science)
Real-time data processing
Autonomous distributed systems
Formal methods (Computer science)
Issue Date: 2008
Publisher: Springer-Verlag
Citation: Cunningham, D., Dietl, W., Drossopoulou, S., Francalanza, A., & Müller, P. (2008). UJ: type soundness for universe types. In F. S. de Boer, M. M. Bonsangue, S. Graf, & W.-P. de Roever (Eds.), Formal Methods for Components and Objects (pp. 1-31). Berlin: Springer-Verlag.
Abstract: Universe types characterise aliasing in object oriented programming languages and are used to reason modularly about programs. In this report we formalise prior work by M ̈uller and Poetzsch-Heffter, who designed the Universe Type System for a core subset of Java. We present our work in two steps. We first give a Topological Universe Type System and show subject reduction to a small-step dynamic semantics for our language. Motivated by concerns of Modular verification, we then give an Encapsulation Universe Type System (based on the owner-as-modifier principle), prove subject reduction with respect to the former small-step semantics, and show how the type system can be used for modular verification.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
UJ_Type_Soundness_for_Universe_Types (1).pdf315.37 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.