A type system for Java bytecode subroutines

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A type system for Java bytecode subroutines

Full text

Pdf (1.26 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

San Diego, California, United States

Pages: 149 - 160

Year of Publication: 1998

ISBN:0-89791-979-3

Authors

Raymie Stata	Digital Equipment Corporation, Systems Research Center
Martín Abadi	Digital Equipment Corporation, Systems Research Center

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 16, Citation Count: 39

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/268946.268959 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	Coh97	Richard M. Cohen. Defensive Java Virtual Machine version 0.5 alpha release. Web pages at http://w~, cli. com/~ May 13, 1997.
	DE97	Sophia Drossopoulou and Susan Eisenbach. Java is type safe---probably. In Proceedings of ECOOP'gT, pages 389-418, June 1997.
	LY96	Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
	Mor95	Grog Morrisett. Compiling with Types. PhD the.. sis, Carnegie Mellon University, December 1995.
	MTC+96	G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL/ML compiler: Performance and safety through types. In Workshop on Compiler Support for Systems Software, 1996.
	Qia97	Zhenyu Qian. A formal specification of Java(tin) Virtual Machine instructions (draft). Web page at http://~w.informatik.uni-bremen . de/-qian/abs-f sjvm. html, 1997.
	Sar97	Vijay Saraswat. The Java bytecode verification problem. Web page at htep:/}w~w.research . art. com/-vj/main.html, 1997.
	SMB97	Emin G~in Sizex, Scan McDirmid, and Brian Bershad. Kimerm A Java system security architecture. Web pages at htzp://kiraera, es . washington, edu/~ 1997.
	Sym97	I)on Syme. Proving Java type soundness, Technical Report 427, University of Cambridge Computer Laboratory, June t{}97.
	TIC97	ACM SIGPLAN Workshop on Types in Compilation (TIC97). June 1997.
	Yel97	Frank Yellin. Private communication. March 1997.

CITED BY 39

	Phillip M. Yelland, A compositional account of the Java virtual machine, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.57-69, January 20-22, 1999, San Antonio, Texas, United States
	Andrew D. Gordon , Don Syme, Typing a multi-language intermediate code, ACM SIGPLAN Notices, v.36 n.3, p.248-260, March 2001
	Stephen N. Freund , John C. Mitchell, A formal framework for the Java bytecode language and verifier, ACM SIGPLAN Notices, v.34 n.10, p.147-166, Oct. 1999
	Todd B. Knoblock , Jakob Rehof, Type elaboration and subtype completion for Java bytecode, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-242, January 19-21, 2000, Boston, MA, USA
	Stephen N. Freund , John C. Mitchell, A type system for object initialization in the Java bytecode language, ACM SIGPLAN Notices, v.33 n.10, p.310-327, Oct. 1998
	Sophia Drossopoulou , David Wragg , Susan Eisenbach, What is Java binary compatibility?, ACM SIGPLAN Notices, v.33 n.10, p.341-361, Oct. 1998
	P. Bieber , J. Cazin , P. Girard , J.-L. Lanet , V. Wiels , G. Zanon, Checking secure interactions of smart card applets: extended version, Journal of Computer Security, v.10 n.4, p.369-398, December 2002
	Tomoyuki Higuchi , Atsushi Ohori, Java bytecode as a typed term calculus, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.201-211, October 06-08, 2002, Pittsburgh, PA, USA
	Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, ACM SIGPLAN Notices, v.37 n.5, May 2002
	Allen Goldberg, A specification of Java loading and bytecode verification, Proceedings of the 5th ACM conference on Computer and communications security, p.49-58, November 02-05, 1998, San Francisco, California, United States
	Robert O'Callahan, A simple, comprehensive type system for Java bytecode subroutines, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-78, January 20-22, 1999, San Antonio, Texas, United States
	Emin Gün Sirer , Robert Grimm , Arthur J. Gregory , Brian N. Bershad, Design and implementation of a distributed virtual machine for networked computers, ACM SIGOPS Operating Systems Review, v.33 n.5, p.202-216, Dec. 1999
	Gleb Naumovich, A conservative algorithm for computing the flow of permissions in Java programs, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
	Gerwin Klein , Tobias Nipkow, Verified bytecode verifiers, Theoretical Computer Science, v.298 n.3, p.583-626, 11 April 2003
	Stéphane Doyon , Mourad Debbabi, Verifying object initialization in the Java bytecode language, Proceedings of the 2000 ACM symposium on Applied computing, p.821-830, March 2000, Como, Italy
	Todd B. Knoblock , Jakob Rehof, Type elaboration and subtype completion for Java bytecode, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.2, p.243-272, March 2001
	Emin Gün Sirer , Brian N. Bershad, Using production grammars in software testing, ACM SIGPLAN Notices, v.35 n.1, p.1-13, Jan. 2000
	Tatsurou Sekiguchi , Takahiro Sakamoto , Akinori Yonezawa, Portable implementation of continuation operators in imperative languages by exception handling, Advances in exception handling techniques, Springer-Verlag New York, Inc., New York, NY, 2001
	Hongwei Xi , Songtao Xia, Towards array bound check elimination in Java ^TM virtual machine language, Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p.14, November 08-11, 1999, Mississauga, Ontario, Canada
	G. Klein , M. Wildmoser, Verified Bytecode Subroutines, Journal of Automated Reasoning, v.30 n.3-4, p.363-398, 2003
	Egon Börger , Wolfram Schulte, A Practical Method for Specification and Analysis of Exception Handling-A Java/JVM Case Study, IEEE Transactions on Software Engineering, v.26 n.9, p.872-887, September 2000
	Atsushi Ohori, Register allocation by proof transformation, Science of Computer Programming, v.50 n.1-3, p.161-187, March 2004
	Tim Sheard, Languages of the future, ACM SIGPLAN Notices, v.39 n.12, December 2004
	Tomoyuki Higuchi , Atsushi Ohori, A static type system for JVM access control, ACM SIGPLAN Notices, v.38 n.9, p.227-237, September 2003
	Antoine Requet, A B model for ensuring soundness of a large subset of the java card virtual machine, Science of Computer Programming, v.46 n.3, p.283-306, March 2003
	Tim Sheard, Languages of the future, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA
	Xinyu Feng , Zhong Shao , Alexander Vaynberg , Sen Xiang , Zhaozhong Ni, Modular verification of assembly code with stack-based control abstractions, ACM SIGPLAN Notices, v.41 n.6, June 2006
	Algis Rudys , Dan S. Wallach, Termination in language-based systems, ACM Transactions on Information and System Security (TISSEC), v.5 n.2, p.138-168, May 2002
	Eva Rose, Lightweight Bytecode Verification, Journal of Automated Reasoning, v.31 n.3-4, p.303-334, 2003
	Zhenyu Qian, Standard fixpoint iteration for Java bytecode verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.638-672, July 2000
	Pieter H. Hartel , Luc Moreau, Formalizing the safety of Java, the Java virtual machine, and Java card, ACM Computing Surveys (CSUR), v.33 n.4, p.517-558, December 2001
	Emin Gün Sirer , Brian N. Bershad, Using production grammars in software testing, Proceedings of the 2nd conference on Conference on Domain-Specific Languages, p.1-1, October 03-05, 1999, Austin, Texas
	Yutaka Matsuno , Atsushi Ohori, A type system equivalent to static single assignment, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy
	Gerwin Klein , Tobias Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.619-695, July 2006
	Tomoyuki Higuchi , Atsushi Ohori, A static type system for JVM access control, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.1, p.4-es, January 2007
	Christian Skalka, Type safe dynamic linking for JVM access control, Proceedings of the 9th ACM SIGPLAN international symposium on Principles and practice of declarative programming, July 14-16, 2007, Wroclaw, Poland
	Pratibha Permandla , Michael Roberson , Chandrasekhar Boyapati, A type system for preventing data races and deadlocks in the java virtual machine language: 1, ACM SIGPLAN Notices, v.42 n.7, July 2007
	Christian Collberg , Ginger Myles , Michael Stepp, An empirical study of Java bytecode programs, Software—Practice & Experience, v.37 n.6, p.581-641, May 2007
	Atsushi Ohori, A proof theory for machine code, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.6, p.36-es, October 2007