Rowe, Reuben N.S., van Bakel, S.J. (2014) Semantic Types and Approximation for Featherweight Java. Theoretical Computer Science, 517 . pp. 34-74. ISSN 0304-3975. (doi:10.1016/j.tcs.2013.08.017) (KAR id:65743)
PDF
Author's Accepted Manuscript
Language: English
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
|
|
Download this file (PDF/460kB) |
|
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: https://doi.org/10.1016/j.tcs.2013.08.017 |
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.
Item Type: | Article |
---|---|
DOI/Identification number: | 10.1016/j.tcs.2013.08.017 |
Uncontrolled keywords: | Featherweight Java; Intersection types; Approximation semantics; Derivation reduction; Strong normalisation |
Subjects: |
Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Reuben Rowe |
Date Deposited: | 17 Jan 2018 11:38 UTC |
Last Modified: | 05 Nov 2024 11:03 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/65743 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):