Department of Computer Science and Technology – Technical reports: UCAM-CL-TR-563 Skip to content | Access key help Search Advanced search A–Z Contact us Department of Computer Science and Technology Computer Laboratory Technical reports UCAM-CL-TR-563 Technical reports MJ: An imperative core calculus for Java and Java with effects G.M. Bierman, M.J. Parkinson, A.M. Pitts April 2003, 53 pages DOI: 10.48456/tr-563 Abstract In order to study rigorously object-oriented languages such as Java or C#, a common practice is to define lightweight fragments, or calculi, which are sufficiently small to facilitate formal proofs of key properties. However many of the current proposals for calculi lack important language features. In this paper we propose Middleweight Java, MJ, as a contender for a minimal imperative core calculus for Java. Whilst compact, MJ models features such as object identity, field assignment, constructor methods and block structure. We define the syntax, type system and operational semantics of MJ, and give a proof of type safety. In order to demonstrate the usefulness of MJ to reason about operational features, we consider a recent proposal of Greenhouse and Boyland to extend Java with an effects system. This effects system is intended to delimit the scope of computational effects within a Java program. We define an extension of MJ with a similar effects system and instrument the operational semantics. We then prove the correctness of the effects system; a question left open by Greenhouse and Boyland. We also consider the question of effect inference for our extended calculus, detail an algorithm for inferring effects information and give a proof of correctness. Full text PDF (0.5 MB) BibTeX record
@TechReport{UCAM-CL-TR-563,
author = {Bierman, G.M. and Parkinson, M.J. and Pitts, A.M.},
title = {{MJ: An imperative core calculus for Java and Java with
effects}},
year = 2003,
month = apr,
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-563.pdf},
institution = {University of Cambridge, Computer Laboratory},
doi = {10.48456/tr-563},
number = {UCAM-CL-TR-563}
}
© 2021 Department of Computer Science and Technology, University of Cambridge Information provided by [Javascript required] Usage licence
