Mobile Resource Guarantees
(MRG, project IST-2001-33149)

Related Publications

Marin Abadi and Rustan Leino. A Logic of Object-Oriented Programs. In TAPSOFT '97 - Theory and Practice of Software Development, 7th International Joint Conference {CAAP/{FASE}}, Lille, France, pages 682-696, LNCS 1214, Springer-Verlag, 1997. (local copy)

Andrew W. Appel and Edward W. Felten. Proof-carrying authentication. In Proceedings of the 6th ACM Conference on Computer and Communications Security, November 1999.

Andrew W. Appel and Amy P. Felty. A semantic model of types and machine instructions for proof-carrying code. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '00), pages 243-253, January 2000.

S. Arora, R. Motwani, M. Safra, M. Sudan, and M. Szegedy. Proof verification and the hardness of approximation problems. Journal of the ACM, 45(3): 501-555, May 1998. Also in Proc. 33rd IEEE Symp. on Foundations of Computer Science, pages 13-22, 1992.

Sanjeev Arora. Probabilistic Checking of Proofs and Hardness of Approximation Problems. PhD thesis, UC Berkeley, 1994. UCB Technical Report: CS-TR-476-94.

David Aspinall and Adriana Compagnoni. Heap bounded assembly language. Submitted, 2001.

Lennart Augustsson. Cayenne - a language with dependent types. In ICFP '98: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, pages 239-250. ACM Press, 1998.

S. Bellantoni, K.-H. Niggl, and H. Schwichtenberg. Ramification, Modality, and Linearity in Higher Type Recursion. Annals of Pure and Applied Logic, 2000. to appear.

Stephen Bellantoni and Stephen Cook. New recursion-theoretic characterization of the polytime functions. Computational Complexity, 2:97-110, 1992.

G. Bellè and E. Moggi. Typed intermediate languages for shape-analysis. In Typed Lambda Calculi and Applications: Proceedings of the Third International Conference TLCA '97, number 1210 in Lecture Notes in Computer Science, pages 11-29. Springer-Verlag, April 1997.

P. Nick Benton, Andrew Kennedy, and George Russell. Compiling Standard ML to Java bytecodes. In ICFP '98: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming. ACM Press, 1998.

Ralph Benzinger. Automatic complexity analysis revisited. Slides for a talk at Cornell University. January 2000.

Gordon Brebner. Circlets: Circuits as applets. In IEEE Symposium on FPGAs for Custom Computing Machines, April 1998. Napa Valley, California.

Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. Comparing object encodings. In Theoretical Aspects of Computer Software (TACS), Sendai, Japan, September 1997. An earlier version was presented as an invited lecture at the Third International Workshop on Foundations of Object Oriented Languages (FOOL 3), July 1996.

A. Coglio, A. Goldberg, and Z. Qian. Toward a provably-correct implementation of the JVM bytecode verifier. Proc. DARPA Information Survivability Conference and Exposition (DISCEX'00), Vol. 2, pages 403-410, IEEE Computer Society, 2000.

Christopher Colby, Peter Lee, and George C. Necula. A Proof-Carrying Code architecture for Java. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV00), Chicago, 2000.

Adriana Compagnoni. CAREER: A formally verified environment for the production of secure software. NSF project based at Stevens Institute of Technology, Hoboken, New Jersey. 2000.

K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. TALx86: A realistic typed assembly language. In 1999 ACM SIGPLAN Workshop on Compiler Support for System Software Atlanta, GA, USA, pages 25-35, May 1999.

K. Crary and S. Weirich. Resource bound certification. In Proc. 27th Symp. Principles of Prog. Lang. (POPL), pages 184-198. ACM, 2000.

S. Freund and J. Mitchell. A formal framework for the Java bytecode language and verifier. ACM Conference on Object-Oriented Programming: Systems, Languages and Applications, Denver, CO, November, 1999, pages 147-166.

A. Galland, D. Deville, G. Grimaud and B. Folliot. Contr?le des ressources dans les cartes à microprocesseur. 1er congrès "Logiciel Temps Réels Embarqués", Toulouse, 2002.

Stephen Gilmore. Deep type inference for mobile functions. In P. Trinder G. Michaelson and H.-W. Loidl, editors, Trends in Functional Programming (Volume 1), pages 40-48, 2000.

Stephen Gilmore and Jane Hillston. The PEPA workbench: A tool to support a process algebra-based approach to performance modelling. In Proceedings of the Seventh International Conference on Modelling Techniques and Tools for Computer Performance Evaluation, Springer LNCS vol. 794, pages 353-368, 1994.

Stephen Gilmore and Marco Palomino. BabylonLite: Improvements to a Java-based distributed object system. Submitted to Concurrency and Computation: Practice and Experience, March 2001.

Algorithmic Solutions Software GmbH. LEDA - Library of Efficient Data types and Algorithms. A C++ class library originally developed at the Max-Planck-Institut für Informatik.

A. Gordon and D. Syme. Typing a multi-language intermediate code. Technical Report MSR TR 2000-106, Microsoft Research, 2000. A shorter version appears in Proceedings of Symposium on Principles of Programming Languages, (POPL2001), London, 2001.

GSF. The diabcard project. 2000.

R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. JACM, 40(1):143-184, 1993.

Prahladh Harsha and Madhu Sudan. Small pcps with low query complexity. Electronic Colloquium on Computational Complexity, 2000. Report No. 61.

P. Hartel and L. Moreau Formalizing the Safety of Java, the Java Virtual Machine and Java Card. ACM Computing Surveys 33:517-558 (2001).

Jane Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.

Martin Hofmann. Linear types and non size-increasing polynomial time computation. To appear in Theoretical Computer Science. An extended abstract has appeared under the same title in Proc. Symp. Logic in Comp. Sci. (LICS) 1999, Trento, 2000.

Martin Hofmann. Safe recursion with higher types and BCK-algebra. Annals of Pure and Applied Logic, 2000. to appear.

Martin Hofmann. A type system for bounded space and functional in-place update. Nordic Journal of Computing 7(4):258-289, Winter 2000. A previous version was in: G. Smolka, editor, Programming Languages and Systems, pages 165-179. Springer LNCS, 2000. An

J. Hughes and L. Pareto. Recursion and dynamic data structures in bounded space: towards embedded ML programming. In Proc. International Conference on Functional Programming (ACM). Paris, September '99., pages 70-81, 1999.

Pankaj Kakkar, Michael Hicks, Jonathan T. Moore, and Carl A. Gunter. Specifying the PLAN networking programming language. In Higher Order Operational Techniques in Semantics, volume 26 of Electronic Notes in Theoretical Computer Science. Elsevier, September 1999.

K. Rustan M. Leino. Recursive object types in a logic of object-oriented programs. Nordic Journal of Computing, 5(4):330-360, 1998. (local copy)

J.-Y. Marion and J.-Y. Moyen. Efficient first-order functional program interpreter with time bound certifications. In LPAR 2000, Springer LNAI, 2000.

James McKinna. Deliverables: A Categorical Approach to Program Development in Type Theory. PhD thesis, University of Edinburgh, 1992. Report CST-96-92.

Sun Microsystems. JavaCard software distribution and manuals.

Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, August 1978.

Aloysius K. Mok and Weijiang Yu. TINMAN: A Resource Bound Security Checking System for Mobile Code. Proc. 7th European Symposium on Research in Computer Security, Zurich. Springer LNCS 2502, October 2002.

G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL/ML compiler: Performance and safety through types. 1996 Workshop on Compiler Support for Systems Software, January 1996.

G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems,, 21(3):528-569, May 1999.

Alan Mycroft and Richard Sharp. A statically allocated parallel functional language. In Automata, Languages and Programming, pages 37-48, 2000.

George Necula. Proof-carrying code. In Proceedings of the ACM Symposium on Principles of Programming Languages, 1997.

George Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, September 1998.

George C. Necula and Peter Lee. Safe, untrusted agents using proof-carrying code. In LNCS 1419: Special Issue on Mobile Agent Security. Springer, 1998. Abstract.

George C. Necula and Robert R. Schneck. A Sound Framework for Untrusted Verification-Condition Generators. In Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science, pages 248-260. Computer Society Press, 2003.

T. Nipkow, D. von Oheimb, and C. Pusch. microJava: Embedding a programming language in a theorem prover. In F.L. Bauer and R. Steinbrüggen, editors, Foundations of Secure Computation. Proc. Int. Summer School Marktoberdorf 1999, pages 117-144. IOS Press, 2000.

S. Owre, J. Rushby, and N. Shankar. PVS: a prototype verification system. In Proc. 11th Intl. Conf. on Automated Deduction, Springer LNCS vol. 607, pages 748-752, 1992.

Jens Palsberg and Michael Schwartzbach. Object-oriented type inference. In Proc. ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), pages 246-161, 1991.

Jens Palsberg, Mitchell Wand, and Patrick O'Keefe. Type inference with non-structural subtyping. Formal Aspects of Computing, 9:49-67, 1997.

Lawrence C. Paulson. Isabelle - A Generic Theorem Prover. Lecture Notes in Computer Science 828. Springer-Verlag, 1994. For latest materials, see the Isabelle webpages. A new Isabelle book is in preparation.

Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In Proc. of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98), LNCS 1384, pages 151-166, 1998.

J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS'02 - Symposium on Logic in Computer Science, Copenhage, Denmark, July 22--25, 2002. (local copy)

J. C. Reynolds. Syntactic control of interference. In Proc. Fifth ACM Symp. on Princ. of Prog. Lang. (POPL), 1978.

Raymie Stata and Martin Abadi. A type system for Java bytecode subroutines. In ACM Transactions on Programming Languages and Systems 21, volume 21(1), January 1999.

Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and Computation111:245-296, 1994.

D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation, SIGPLAN Notices, 31(6). ACM Press, June 1996.

Philip Wadler. Linear types can change the world! In TC 2 Working Conference on Programming Concepts and Methods (Preprint), pages 546-566, 1990.

Hongwei Xi and Robert Harper. A dependently typed assembly language. Proc. ICFP, Florence. September, 2001.