Principals in programming languages: a syntactic proof technique

ABSTRACT

Programs are often structured around the idea that different pieces of code comprise distinct principals, each with a view of its environment. Typical examples include the modules of a large program, a host and its clients, or a collection of interactive agents.In this paper, we formalize this notion of principal in the programming language itself. The result is a language in which intuitive statements such as, "the client must call open to obtain a file handle," can be phrased and proven formally.We add principals to variants of the simply-typed λ-calculus and show how we can track the code corresponding to each principal throughout evaluation. This multiagent calculus yields syntactic proofs of some type abstraction properties that traditionally require semantic arguments.

REFERENCES

• 1: Martín Abadi , Luca Cardelli , Pierre-Louis Curien, Formal parametric polymorphism, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.157-170, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158622]
• 2: Godmar Back, Patrick Tullmann, Leigh Stoller, Wilson C. Hseih, and Jay Lepreau. Java operating systems: Design and implementation. Technical Report UUCS-98-015, University of Utah, August 1998.
• 3: 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
• 4: Karl Crary, A simple proof technique for certain parametricity results, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.82-89, September 27-29, 1999, Paris, France
• 5: Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
• 6: Michael Godfrey , Tobias Mayr , Praveen Seshadri , Thorsten von Eicken, Secure and portable database extensibility, Proceedings of the 1998 ACM SIGMOD international conference on Management of data, p.390-401, June 01-04, 1998, Seattle, Washington, United States
• 7: Chris Hawblitzel, Chi-Chao Chang, Grzegorz Czajkowski, Deyu Hu, and Thorston yon Eiken. Implementing multiple protection domains in /lava.. In 1998 USENiX Annual Technical Conference, New Orleans, LA, June 1998.
• 8: Nevin Heintze , Jon G. Riecke, The SLam calculus: programming with secrecy and integrity, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.365-377, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268976]
• 9: 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]
• 10: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 11: John C. Mitchell, On the equivalence of data representations, Artificial intelligence and mathematical theory of computation: papers in honor of John McCarthy, Academic Press Professional, Inc., San Diego, CA, 1991
• 12: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• 13: Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292561]
• 14: Flemming Nielson , Hanne Riis Nielson, Two-level functional languages, Cambridge University Press, New York, NY, 1992
• 15: John Peterson, Kevin Hammond, Lennart Augustsson, Brian Boutel, Warren Burton, Joseph Fasel~, Andrew D. Gordon, John Hughes, Paul Hudak, Thomas Johnsson, Mark Jones, Erik Meijer, Simon Peyton Jones, Alastair Reid, and Philip Wadler. Report on the programming language Haskell, version 1.4. http://www.haskell.org/report.
• 16: Benjamin C. Pierce and Deride Sangiorgi. Behavioral equivalence in the polymorphic pi-calculus. Technical Report MS- CIS-99-10, University of Pennsylvania, April 1999.
• 17: John Hamilton Reppy. Higher-order Concurrency. PhD thesis, Cornell University, Ithaca, NY, June 1992. TR 92-1852.
• 18: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 19: John C. Reynolds. Types, abstraction, and parametric polymorphism. In R.E.A Mason, editor, Information Processing, pages 513-523. Elsevier Science Publishers B.V., 1983.
• 20: C. Strachey. Fundamental concepts in programming languages. Unpublished Lecture Notes, Summer School in Computer Programming, August 1967.
• 21: Dennis M. Volpano , Geoffrey Smith, A Type-Based Approach to Program Security, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.607-621, April 14-18, 1997
• 22: Dan S. Wallach and Edward W. Felten. Understanding Java stack inspection. In Proceedings oj' 1998 IEEE Symposium on Security and Privacy, Oakland, CA, May 1998.
• 23: Dan Seth Wallach. A New Approach to Mobile Code Security. PhD thesis, Princeton University, 1999.
• 24: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
• 25: Steve Zdancewic and Dan Grossman. Syntax and semantics for multiple agents and abstract types. Technical Report 99-1752, Cornell University, March 1999.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Languages, Theory