Syntactic type abstraction

ABSTRACT

Software developers often structure programs in such a way that different pieces of code constitute distinct principals. Types help define the protocol by which these principals interact. In particular, abstract types allow a principal to make strong assumptions about how well-typed clients use the facilities that it provides. We show how the notions of principals and type abstraction can be formalized within a language. Different principals can know the implementation of different abstract types. We use additional syntax to track the flow of values with abstract types during the evaluation of a program and demonstrate how this framework supports syntactic proofs (in the sytle of subject reduction) for type-abstraction properties. Such properties have traditionally required semantic arguments; using syntax aboids the need to build a model and recursive typesfor the language. We present various typed lambda calculi with principals, including versions that have mutable state and recursive types.

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: Abadi, M. and Plotkin, G. D. 1990. A PER model of polymorphism. In 5th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 355-365.
• 3: Thierry Coquand , Carl A. Gunter , Glynn Winskel, DI-Domains as a Model of Polymorphism, Proceedings of the 3rd Workshop on Mathematical Foundations of Programming Language Semantics, p.344-363, April 08-10, 1987
• 4: Thierry Coquand , Carl Gunter, Domain theoretic models of polymorphism, Information and Computation, v.81 n.2, p.123-167, May 1989 [doi>10.1016/0890-5401(89)90068-0]
• 5: 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
• 6: Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
• 7: 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]
• 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: QingMing Ma , John C. Reynolds, Types, Abstractions, and Parametric Polymorphism, Part 2, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.1-40, March 25-28, 1991
• 11: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
• 12: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 13: 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
• 14: 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]
• 15: Morrisett, G. 1995. Compiling with types. Ph.D. thesis, Carnegie Mellon University. Published as CMU Tech Report number CMU-CS-95-226.
• 16: 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]
• 17: Flemming Nielson , Hanne Riis Nielson, Two-level functional languages, Cambridge University Press, New York, NY, 1992
• 18: Peyton Jones, S., Hughes, J., Augustsson, L., Barton, D., Boutel, B., Fasel, J., Hammond, K., Hinze, R., Hudak, P., Johnsson, T., Jones, M., Launchbury, J., Meijer, E., Peterson, J., Reid, A., Runciman, C., and Wadler, P. 1999. Haskell 98: A non-strict, purely functional language. http://www.haskell.org/onlinereport/.
• 19: Benjamin C. Pierce , Davide Sangiorgi, Behavioral equivalence in the polymorphic pi-calculus, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.242-255, January 15-17, 1997, Paris, France [doi>10.1145/263699.263729]
• 20: Pitts, A. M. 1996. Relational properties of domains. Inf. Comput. 127, 66-90.
• 21: Andrew M. Pitts, Parametric polymorphism and operational equivalence, Mathematical Structures in Computer Science, v.10 n.3, p.321-359, June 2000 [doi>10.1017/S0960129500003066]
• 22: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 23: Reynolds, J. C. 1983. Types, abstraction and parametric polymorphism. In Information Processing 83, R. E. A. Mason, Ed. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 513-523.
• 24: Sewell, P. and Vitek, J. 1999. Secure composition of untrusted code with wrappers and causality types. Work in Progress http://www.cs.purdue.edu/homes/jv/publist.html.
• 25: Strachey, C. 1967. Fundamental concepts in programming languages. Unpublished Lecture Notes, Summer School in Computer Programming.
• 26: 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
• 27: 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]
• 28: Steve Zdancewic , Dan Grossman , Greg Morrisett, Principals in programming languages: a syntactic proof technique, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.197-207, September 27-29, 1999, Paris, France

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Information hiding

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Languages (e.g., description, interconnection, definition)
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax; Semantics
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Security, Theory, Verification

Keywords:
operational semantics, parametricity, proof techniques, syntactic proofs, type abstraction