Dan Grossman
Greg Morrisett
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.
- Abadi, M., Cardelli, L., and Curien, P.-L. 1993. Formal parametric polymorphism. In 20th ACM Symposium on Principles of Programming Languages. ACM Press, New York, NY, 157- 167. Google Scholar
- 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.Google Scholar
- Coquand, T., Gunter, C. A.,and Winskel, G. 1987. DI-domains as a model of polymorphism. In Mathematical Foundations of Programming Language Semantics, M. Main, A. Melton, M. Mislove, and D. A. Schmidt, Eds. Lecture Notes in Computer Science, vol. 298. Springer- Verlag, New York, NY, 344-363. Google Scholar
- Coquand, T., Gunter, C. A., and Winskel, G. 1989. Domain theoretic models of polymorphism. Inf. Comput. 81, 2 (May), 123-167. Google Scholar
- Crary, K. 1999. A simple proof technique for certain parametricity results. In 4th ACM International Conference on Functional Programming. ACM Press, New York, NY, 82-89. Google Scholar
- Girard, J.-Y., Lafont, Y., and Taylor, P. 1989. Proofs and Types. Cambridge University Press, Cambridge, UK. Google Scholar
- Harper, R. 1994. A simplified account of polymorphic references. Information Processing Letters 51, 4 (August), 201-206. Google Scholar
- Heintze, N. and Riecke, J. G. 1998. The SLam calculus: programming with secrecy and integrity. In 25th ACM Symposium on Principles of Programming Languages. ACM Press, New York, NY, 365-377. Google Scholar
- Leroy, X. and Rouaix, F. 1998. Security properties of typed applets. In 25th ACM Symposium on Principles of Programming Languages. ACM Press, New York, NY, 391-403. Google Scholar
- Ma, Q. and Reynolds, J. 1992. Types, abstraction, and parametric polymorphism: Part 2. In Proceedings of the 1991 Mathematical Foundations of Programming Semantics, S. Brookes, M. Main, A. Melton, M. Mislove, and D. A. Schmidt, Eds. Number 598 in Lecture Notes in Computer Science. Springer-Verlag, New York, NY, 1-40. Google Scholar
- MacQueen, D., Plotkin, G. D., and Sethi, R. 1986. An ideal model for recursive polymorphism. Information and Control 71, 1/2 (October/November), 95-130. Google Scholar
- Milner, R., Tofte, M., Harper, R., and MacQueen, D. 1997. The Definition of Standard ML (Revised). The MIT Press, Cambridge, MA. Google Scholar
- Mitchell, J. 1991. On the equivalence of data representations. In Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, V. Lifschitz,Ed. Academic Press, San Diego, CA, 305-330. Google Scholar
- Mitchell, J. C. and Plotkin, G. D. 1988. Abstract types have existential type. ACM Transactions on Programming Languages and Systems 10, 3 (July), 470-502. Google Scholar
- Morrisett, G. 1995. Compiling with types. Ph.D. thesis, Carnegie Mellon University. Published as CMU Tech Report number CMU-CS-95-226.Google Scholar
- Myers, A. C. 1999. JFlow: Practical mostly-static information ow control. In 26th ACM Symposium on Principles of Programming Languages. ACM Press, New York, NY, 228-241. Google Scholar
- Nielson, F. and Nielson, H. R. 1992. Two-Level Functional Languages. Number 34 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK. Google Scholar
- 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/.Google Scholar
- Pierce, B. C. and Sangiorgi, D. 1999. Behavioral equivalence in the polymorphic pi-calculus. Tech. Rep. MS-CIS-99-10, University of Pennsylvania. Apr. (Summary in 24th ACM Symposium on Principles of Programming Languages). Google Scholar
- Pitts, A. M. 1996. Relational properties of domains. Inf. Comput. 127, 66-90.Google Scholar
- Pitts, A. M. 2000. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10, 1-39. Google Scholar
- Reynolds, J. C. 1974. Towards a theory of type structure. In Programming Symposium. Lecture Notes in Computer Science, vol. 19. Springer-Verlag, New York, NY, 408-425. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Strachey, C. 1967. Fundamental concepts in programming languages. Unpublished Lecture Notes, Summer School in Computer Programming.Google Scholar
- Volpano, D. and Smith, G. 1997. A type-based approach to program security. In TAPSOFT'97, Theory and Practice of Software Development. Lecture Notes in Computer Science, vol. 1214. Springer-Verlag, New York, NY. Google Scholar
- Wright, A. K. and Felleisen, M. 1994. A syntactic approach to type soundness. Inf. Comput. 115, 1, 38-94. Preliminary version in Rice Tech. Rep. 91-160. Google Scholar
- Zdancewic, S., Grossman, D., and Morrisett, G. 1999. Principals in programming languages: A syntactic proof technique. In 4th ACM International Conference on Functional Programming. ACM Press, New York, NY, 197-207. Google Scholar
Index Terms
- Syntactic type abstraction
Recommendations
Parametric quantifiers for dependent type theory
Polymorphic type systems such as System F enjoy the parametricity property: polymorphic functions cannot inspect their type argument and will therefore apply the same algorithm to any type they are instantiated on. This idea is formalized mathematically ...
Dynamic Translucency with Abstraction Kinds and Higher-Order Coercions
When a module language is combined with forms of non-parametric type analysis, abstract types require an opaque dynamic representation in order to maintain abstraction safety. As an idealisation of such a module language, we present a foundational ...
Type-preserving CPS translation of Σ and Π types is not not possible
Dependently typed languages such as Coq are used to specify and prove functional correctness of source programs, but what we ultimately need are guarantees about correctness of compiled code. By preserving dependent types through each compiler pass, we ...
Comments