Type-safe linking and modular assembly language

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Type-safe linking and modular assembly language

Full text

Pdf (1.36 MB)

Source

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

San Antonio, Texas, United States

Pages: 250 - 261

Year of Publication: 1999

ISBN:1-58113-095-3

Authors

Neal Glew	Department of Computer Science, Cornell University
Greg Morrisett	Department of Computer Science, Cornell University

Sponsors

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

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 10, Downloads (12 Months): 31, Citation Count: 23

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/292540.292563 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.

	BSP+95	B. N. Bershad , S. Savage , P. Pardyak , E. G. Sirer , M. E. Fiuczynski , D. Becker , C. Chambers , S. Eggers, Extensibility safety and performance in the SPIN operating system, Proceedings of the fifteenth ACM symposium on Operating systems principles, p.267-283, December 03-06, 1995, Copper Mountain, Colorado, United States
	Car88	L. Cardelli, Structural subtyping and the notion of power type, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-79, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73566]
	Car91	Luca Cardelli. Typeful programming. In Formal Description of Programming Concepts. Springer-Verlag, 1991.
	Car97	Luca Cardelli, Program fragments, linking, and modularization, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.266-277, January 15-17, 1997, Paris, France [doi>10.1145/263699.263735]
	Cra98	Karl Fredrick Crary , Robert L. Constable, Type-theoretic methodology for practical programming languages, 1998
	DE98a	Sophia DrossopouIou and Susan Eisenbach. Is the Java type system sound? In Theory and Practice of Object systems, 1998. To appear, available at http://www-dse, doc. ic. ac. uk/proj e c~ s/slurp/.
	DE98b	Sophia Drossopoulou and Susan Eisenbach. Towards an Operational Semantics and a Proof of Type Soundness for Java. Springer-Verlag, 1998. To appear, available at ht~p ://w~a-dse. doc. ic. ac. uk/pro j ect s/slurp/.
	Dea97	Drew Dean, The security of static typing with dynamic linking, Proceedings of the 4th ACM conference on Computer and communications security, p.18-27, April 01-04, 1997, Zurich, Switzerland [doi>10.1145/266420.266428]
	DS98	Dominic Duggan and Constantinos Sourelis. Parameterized modules, recursive modules and mixin modules. In ACM SIGPLAN Workshop on ML, pages 87-96, Baltimore, MA, USA, September 1998.
	FF98	Matthew Flatt , Matthias Felleisen, Units: cool modules for HOT languages, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.236-248, June 17-19, 1998, Montreal, Quebec, Canada
	Gir71	Jean-Yves Girard. Une extension de l'interpr6tation de G6del ~ l'analyse, et son application ~ l'~limination de coupures dans l'analyse et la th6orie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 63-92. North-Holland Publishing Co., 1971.
	Gir72	Jean-Yves Girard. Interprdtation fonctionelle et dlimination des coupures de l'arithmdtique d'ordre supdrieur. PhD thesis, Universit6 Paris VII, 1972.
	Har94	Robert Harper, A simplified account of polymorphic references, Information Processing Letters, v.51 n.4, p.201-206, Aug. 24, 1994 [doi>10.1016/0020-0190(94)90120-1]
	HCC+98	Chris Hawblitzel, Chi-Chao Chang, Grzegorz Czajkowski, Deyu Hu, and Thorsten yon Eicken. Implementing multiple protection domains in Java. In 1998 USENIX Annual Technical Conference, New Orleans, LA, USA, June 1998.
	HL94	Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176927]
	HMM90	Robert Harper , John C. Mitchell , Eugenio Moggi, Higher-order modules and the phase distinction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.341-354, December 1989, San Francisco, California, United States [doi>10.1145/96709.96744]
	Koz98	Dexter Kozen, Efficient Code Certification, Cornell University, Ithaca, NY, 1998
	Ler94	Xavier Leroy, Manifest types, modules, and separate compilation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-122, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176926]
	LR98	Xavier Leroy , François Rouaix, Security properties of typed applets, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.391-403, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268979]
	LY97	Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
	MCGW98	J. Gregory Morrisett , Karl Crary , Neal Glew , David Walker, Stack-Based Typed Assembly Language, Proceedings of the Second International Workshop on Types in Compilation, p.28-52, March 25-27, 1998
	MF96	Gary McGraw , Edward W. Felten, Java security: hostile applets, holes&antidotes, John Wiley & Sons, Inc., New York, NY, 1997
	Mil91	Robert Milner. The polyadic 1r-calculus: a tutorial. Technical Report ECS-LCFS-91-180, Edinburgh University, 1991. Reprinted in Logic and Algebra of Specification, F. Brauer, W. Brauer, and H. Schwichtenberg, Eds, Springer Verlag, 1993, 203-246.
	MWCG97	Greg Morrisett , David Walker , Karl Crary , Neal Glew, From System F to Typed Assembly Language (Extended Version), Cornell University, Ithaca, NY, 1997
	MWCG98	Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
	Nec97	George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
	Sar97	Vijay Saraswat. Java is not type-safe. URL: http:// ,w~. research, a~. com/'vj/bug, h~ml, August 1997.
	SFPB96	Emin Gtln Street, Marc Fiuczynski, Przemyslaw Pardyak, and Brian Bershad. Safe dynamic linking in an extensible operating system. In Workshop on Compiler Support for System Software, February 1996.
	Sha98	Zhong Shao, Typed cross-module compilation, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.141-152, September 26-29, 1998, Baltimore, Maryland, United States
	WLAG93	Robert Wahbe , Steven Lucco , Thomas E. Anderson , Susan L. Graham, Efficient software-based fault isolation, Proceedings of the fourteenth ACM symposium on Operating systems principles, p.203-216, December 05-08, 1993, Asheville, North Carolina, United States

CITED BY 23

	Nael B. Abu-Ghazaleh , Dhananjay S. Phatak, Verification caching: towards efficient and secure mobile code execution environments, Proceedings of the 2002 ACM symposium on Applied computing, March 11-14, 2002, Madrid, Spain
	Philip W. L. Fong , Robert D. Cameron, Proof linking: modular verification of mobile programs in the presence of lazy, dynamic linking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.4, p.379-409, Oct. 2000
	Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999
	Dominic Duggan , Ching-Ching Techaubol, Modular mixin-based inheritance for application frameworks, ACM SIGPLAN Notices, v.36 n.11, p.223-240, 11/01/2001
	Zhenyu Qian , Allen Goldberg , Alessandro Coglio, A formal specification of Java class loading, ACM SIGPLAN Notices, v.35 n.10, p.325-336, Oct. 2000
	Dominic Duggan, Type-Safe linking with recursive DLLs and shared libraries, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.6, p.711-804, November 2002
	Peter Sewell , Jan Vitek, Secure composition of untrusted code: box π, wrappers, and causality types, Journal of Computer Security, v.11 n.2, p.135-187, May 2003
	Lujo Bauer , Andrew W. Appel , Edward W. Felten, Mechanisms for secure modular programming in Java, Software—Practice & Experience, v.33 n.5, p.461-480, 25 April 2003
	Philip W. L. Fong, Pluggable verification modules: an extensible protection mechanism for the JVM, ACM SIGPLAN Notices, v.39 n.10, October 2004
	Dominic Duggan, Type-based hot swapping of running modules (extended abstract), ACM SIGPLAN Notices, v.36 n.10, October 2001
	Dachuan Yu , Zhong Shao, Verification of safety properties for concurrent assembly code, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Crispin Cowan , Steve Beattie , Greg Kroah-Hartman , Calton Pu , Perry Wagle , Virgil Gligor, SubDomain: Parsimonious Server Security, Proceedings of the 14th USENIX conference on System administration, December 03-08, 2000, New Orleans, Louisiana
	Akihiko Tozawa , Masami Hagiya, Formalization and Analysis of Class Loading in Java, Higher-Order and Symbolic Computation, v.15 n.1, p.7-55, March 2002
	Peter Sewell, Modules, abstract types, and distributed versioning, ACM SIGPLAN Notices, v.36 n.3, p.236-247, March 2001
	Mark Aiken , Manuel Fähndrich , Chris Hawblitzel , Galen Hunt , James Larus, Deconstructing process isolation, Proceedings of the 2006 workshop on Memory system performance and correctness, October 22-22, 2006, San Jose, California
	Yu David Liu , Scott F. Smith, A formal framework for component deployment, ACM SIGPLAN Notices, v.41 n.10, October 2006
	Saurabh Srivastava , Michael Hicks , Jeffrey S. Foster, Modular information hiding and type-safe linking for C, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France
	Alastair Reid , Matthew Flatt , Leigh Stoller , Jay Lepreau , Eric Eide, Knit: component composition for systems software, Proceedings of the 4th conference on Symposium on Operating System Design & Implementation, p.24-24, October 22-25, 2000, San Diego, California
	David Swasey , Tom Murphy, VII , Karl Crary , Robert Harper, A separate compilation extension to standard ML, Proceedings of the 2006 workshop on ML, September 16-16, 2006, Portland, Oregon, USA
	Hongxu Cai , Zhong Shao , Alexander Vaynberg, Certified self-modifying code, ACM SIGPLAN Notices, v.42 n.6, June 2007
	Gianluigi Ferrari , Eugenio Moggi , Rosario Pugliese, MetaKlaim: a type safe multi-stage language for global computing, Mathematical Structures in Computer Science, v.14 n.3, p.367-395, June 2004
	Davide Ancona , Elena Zucca, A calculus of module systems, Journal of Functional Programming, v.12 n.2, p.91-132, March 2002
	Xavier Leroy, A modular module system, Journal of Functional Programming, v.10 n.3, p.269-303, May 2000