Imperial College London

DrSteffenvan Bakel

Faculty of EngineeringDepartment of Computing

Senior Lecturer
 
 
 
//

Contact

 

+44 (0)20 7594 8263s.van.bakel Website

 
 
//

Location

 

425Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Rowe:2014:10.1016/j.tcs.2013.08.017,
author = {Rowe, RNS and van, Bakel SJ},
doi = {10.1016/j.tcs.2013.08.017},
journal = {Theoretical Computer Science},
pages = {34--74},
title = {Semantic types and approximation for featherweight java},
url = {http://dx.doi.org/10.1016/j.tcs.2013.08.017},
volume = {517},
year = {2014}
}

RIS format (EndNote, RefMan)

TY  - JOUR
AB - We consider semantics for the class-based object-oriented calculus Featherweight Java (without casts) based upon approximation. We also define an intersection type assignment system for this calculus and show that it satisfies subject reduction and expansion, i.e. types are preserved under reduction and its converse. We establish a link between type assignment and the approximation semantics by showing an approximation result, which leads to a sufficient condition for the characterisation of head-normalisation and termination. We show the expressivity of both our calculus and our type system by defining an encoding of Combinatory Logic into our calculus and showing that this encoding preserves typeability. We also show that our system characterises the normalising and strongly normalising terms for this encoding. We thus demonstrate that the great analytic capabilities of intersection types can be applied to the context of class-based object orientation.
AU - Rowe,RNS
AU - van,Bakel SJ
DO - 10.1016/j.tcs.2013.08.017
EP - 74
PY - 2014///
SN - 0304-3975
SP - 34
TI - Semantic types and approximation for featherweight java
T2 - Theoretical Computer Science
UR - http://dx.doi.org/10.1016/j.tcs.2013.08.017
UR - https://www.sciencedirect.com/science/article/pii/S0304397513006415?via%3Dihub
UR - http://hdl.handle.net/10044/1/83345
VL - 517
ER -