A Formal Type System for Java

M. Debbabi and M. Fourati

REFEREED
ARTICLE

Abstract

The primary objective of this paper is threefold: First, we present an evaluation of the state of the art on Java static semantics. Accordingly, we discuss the completeness and the soundness of the most prominent proposals recently advanced in the literature. Moreover, we discuss their compliance with respect to the Java language specification. Second, we report a brief evaluation of the official Java language specification. Third, we show how the definition of a realistic static semantics for full Java could be addressed. We exhibit the technical difficulties and discuss the semantic traits that could be used to address them.

Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.

About the authors

		Mourad Debbabi is a Full Professor at the Concordia Institute for Information Systems Engineering of Concordia University. He is also a Concordia Research Chair Tier I in Information Systems Security. He holds Ph.D. and M.Sc. degrees in computer science from Paris-XI Orsay, University, France. He published more than 120 research papers in international journals and conferences on computer security, formal semantics, mobile and embedded platforms, Java technology security and acceleration, cryptographic protocol specification, design and analysis, malicious code detection, programming languages, type theory and specification and verification of safety-critical systems. In the past, he served as Senior Scientist at the Panasonic Information and Network Technologies Laboratory, Princeton, New Jersey, USA; Associate Professor at the Computer Science Department of Laval University, Quebec, Canada; Senior Scientist at General Electric Corporate Research Center, New York, USA; Research Associate at the Computer Science Department of Stanford University, California, USA; and Permanent Researcher at the Bull Corporate Research Center, Paris, France. See also http://www.ciise.concordia.ca/~debbabi.
		Myriam Fourati is a Ph.D. student at the Computer Science and Software Engineering Department of Laval University, Sainte-Foy, Quebec, Canada. She is also affiliated with the Computer Security Laboratory of Concordia University. She is finishing a Ph.D. thesis under the supervision of Dr. M. Debbabi on trusted self-certified code in Java technology. She has been awarded the President Prize of Tunisia for her research on Java security and semantics. She is also a lecturer at the Faculté des Sciences de Tunis.

Cite this article as follows: M. Debbabi and M. Fourati: "A Formal Type System for Java", in Journal of Object Technology, vol. 6, no. 8, September-October 2007, pages 117-184, http://www.jot.fm/issues/issues 2007 09/article3