Semantic types and approximation for featherweight java
File(s)RvB.pdf (1.87 MB)
Accepted version
Author(s)
Rowe, Reuben NS
van Bakel, SJ
Type
Journal Article
Abstract
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.
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.
Date Issued
2014-01
Date Acceptance
2013-08-22
Citation
Theoretical Computer Science, 2014, 517, pp.34-74
ISSN
0304-3975
Publisher
Elsevier BV
Start Page
34
End Page
74
Journal / Book Title
Theoretical Computer Science
Volume
517
Copyright Statement
© 2020 Elsevier Ltd. All rights reserved. This manuscript is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International Licence http://creativecommons.org/licenses/by-nc-nd/4.0/
Identifier
https://www.sciencedirect.com/science/article/pii/S0304397513006415?via%3Dihub
Subjects
01 Mathematical Sciences
08 Information and Computing Sciences
Computation Theory & Mathematics
Publication Status
Published
Date Publish Online
2013-08-30