Steve Zdancewic
Greg Morrisett
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.
- 1.Martin Abadi, Luca Cardelli, and Pierre-Louis Curien. Formal parametric polymorphism. In Principles of Programming Languages~ volume 20, pages 157-167, January 1993. Google Scholar
Digital Library
- 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.Google Scholar
- 3.Brian N. Bershad, Stefar~ Savage, Przemy'slaw Pardyak, gers, and Craig Chambers. Extensibility, safety and performance in the SPIN operating system, in P~)ceedings o.f the Fifteenth A CM Symposium on Operating Systems Principles, pages 267-283, Copper Mountain, CO, December 1995. Google ScholarDigital Library
- 4.Karl Crary. A simple proof technique for certain parametricity results. In Proceedings of the 4th ArM SIGPLAN international Conference on Functional Programming, Paris, France, September 1999. This volume. Google ScholarDigital Library
- 5.Jean-Yves Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989. Google ScholarDigital Library
- 6.Michael Godfrey, Tobias Mayr, Praveen Seshadri, and Thorsten yon Eicken. Secure and portable database extensibility. In Proceedings of the 1997 ACM-SIGMOD Con/erence on the Management of Data, pages 390-401, Seattle, WA, June 1998. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 8.Nevin Heintze and Jon G. Riecke. The SL~n calculus: programming with secrecy and integrity. In Conference Record o/ the Twenty-Fifth Annual A CM Symposium on Principles of Programming Langu~zges, pages 365-377. ACM Press, 1998. Google ScholarDigital Library
- 9.Xavier Leroy and Fran(:ois Rouajx. Security properties of typed applets. In Principles of Programming Languages, January 1998. Google ScholarDigital Library
- 10.Robin Milner, Muds Tofte, Robert Harper, and David Mac- Queen. The Definition of Standard ML (Revised). The MIT Press, 1997. Google ScholarDigital Library
- 11.J.C. Mitchell. On the equivalence of data representations. in V. Lifschitz, editor, Artificial Intelligence' and Mathematical Theory of Computation: Papers in Honor of John Mc- Carthy, pages 305-330. Academic Press, 1991. Google ScholarDigital Library
- 12.John C. Mitchell and Gordon D. Plotkin. Abstract types have existential type. A GM Transactions on Programming Languages and Systems, 10(3):470-502, July 1988. Google ScholarDigital Library
- 13.Andrew C. Myers. JFlow: Practical mostly-static information flow control. In Proceedings of the 26th A CM Symposium on Principles of Programming Languages, pages 228- 241, San Antonio, TX, January 1999. Google ScholarDigital Library
- 14.Flemming Nielson and Hanne Riis Nielson. Two-Level Functional Languages. Number 34 in Cambridge Tracts in Theoretica~ Computer Science. Cambridge University Press, 1992. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- 17.John Hamilton Reppy. Higher-order Concurrency. PhD thesis, Cornell University, Ithaca, NY, June 1992. TR 92-1852.Google Scholar
- 18.John C. Reynolds. Towards a theory of type structure. In Programming Symposium, volume 19 of Lecture Notes in Computer Science, pages 408-425. Springer-Verlag, Paris, France, April 1974. Google ScholarDigital Library
- 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.Google Scholar
- 20.C. Strachey. Fundamental concepts in programming languages. Unpublished Lecture Notes, Summer School in Computer Programming, August 1967.Google Scholar
- 21.Dennis Volpano and Geoffrey Smith. A type-based approach to program security. In Proceedings of TAPSOFT '97, Colloquium on Formal Approaches to Software Engineering, Lille, France, April 1997. Google ScholarDigital Library
- 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.Google Scholar
- 23.Dan Seth Wallach. A New Approach to Mobile Code Security. PhD thesis, Princeton University, 1999.Google ScholarDigital Library
- 24.Andrew K. Wright and Mattias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38-94, 1994. Preliminary version in Rice TR 91-160. Google ScholarDigital Library
- 25.Steve Zdancewic and Dan Grossman. Syntax and semantics for multiple agents and abstract types. Technical Report 99-1752, Cornell University, March 1999.Google Scholar
Index Terms
- Principals in programming languages: a syntactic proof technique
Recommendations
Principals in programming languages: a syntactic proof technique
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 ...
Higher-order logic programming languages with constraints: a semantics
TLCA'07: Proceedings of the 8th international conference on Typed lambda calculi and applicationsA Kripke Semantics is defined for a higher-order logic programming language with constraints, based on Church's Theory of Types and a generic constraint formalism.
Our syntactic formal system, hoHH(C) (higher-order hereditary Harrop formulas with ...
Logical foundations for more expressive declarative temporal logic programming languages
In this article, we present a declarative propositional temporal logic programming language called TeDiLog that is a combination of the temporal and disjunctive paradigms in logic programming. TeDiLog is, syntactically, a sublanguage of the well-known ...
Comments