From Algol to polymorphic linear lambda-calculus

ABSTRACT

In a linearly-typed functional language, one can define functions that consume their arguments in the process of computing their results. This is reminiscent of state transformations in imperative languages, where execition of an assignment statement alters the contents of the store. We explore this connection by translating two variations on Algol 60 into a purely functional language with polymorphic linear types. On the one hand, the translations lead to a semantic analysis of Algol-like programs, in terms of a model of the linear language. On the other hand, they demonstrate that a linearly-typed functional language can be at least as expressive as Algol.

REFERENCES

• 1: Samson Abramsky, Computational interpretations of linear logic, Theoretical Computer Science, v.111 n.1-2, p.3-57, April 12, 1993 [doi>10.1016/0304-3975(93)90181-R]
• 2: Samson Abramsky , Radha Jagadeesan , Pasquale Malacaria, Full abstraction for PCF, Information and Computation, v.163 n.2, p.409-470, Dec 2000 [doi>10.1006/inco.2000.2930]
• 3: Samson Abramsky , Achim Jung, Domain theory, Handbook of logic in computer science (vol. 3): semantic structures, Oxford University Press, Oxford, 1995
• 4: ABRAMSKY, S., AND McCUSKER, G. 1997 Linearity, sharing and state. In Algol-like Languages, Vol. 2. P. W. O'Hearn and R. D. Tennent, Eds., pp. 297-330. Birkhauser, Boston, Mass.
• 5: BARBER, A., AND PLOTKIN, G. 1997. Dual intuitionistic linear logic. Submitted.
• 6: P. N. Benton , Gavin M. Bierman , Valeria de Paiva , Martin Hyland, A Term Calculus for Intuitionistic Linear Logic, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.75-90, March 16-18, 1993
• 7: Gérard Berry, Stable Models of Typed lambda-Calculi, Proceedings of the Fifth Colloquium on Automata, Languages and Programming, p.72-89, July 17-21, 1978
• 8: BERRY, G., AND CURIEN, P.-L. 1982. Sequential algorithms on concrete data structures. Theoret. Comput. Sci. 20, 265-321.
• 9: Proceedings of the International Conference on Typed Lambda Calculi and Applications, March 1993
• 10: BROOKES, S., MAIN, M., MELTON, A., AND MISLOVE, M. EDS. 1995. Mathematical Foundations of Programming Semantics, Eleventh Annual Conference (Tulane University, New Orleans, March 29-Apr. 1). Elsevier Science, Amsterdam, The Netherlands.
• 11: CHIRIMAR, J., GUNTER, C. A., AND RIECKE, J. 1994. Reference counting as a computational interpretation of linear logic. J. Funct. Prog. 2, 6, 194-244.
• 12: DAY, B.J. 1970. On closed categories of functors. In Reports of the Midwest Category Seminar, S. Mac Lane, ed., Lecture Notes in Mathematics, vol. 137. Springer-Verlag, Berlin-New York, pp. 1-38.
• 13: GIRARD, J.-Y. 1972. Interprdtation Fonctionnelle et Elimination des Coupures de l'Arithmdtique d'Ordre Supdrieur. Ph.D. dissertation. Universit6 Paris VII, Paris, France.
• 14: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 15: HOLMSTRC)M, S. 1988. Linear functional programming. In Proceedings of the Workshop on Implementation of Lazy Functional Languages. Chalmers Univ., Gotenburg, Sweden.
• 16: HYLAND, J. M. E., AND ONG, C.-H. L. 1994. On full abstraction for PCF: I, II and III. Submitted for publication.
• 17: Y. Lafont, The linear abstract machine, Theoretical Computer Science, v.59 n.1-2, p.157-180, July 1988 [doi>10.1016/0304-3975(88)90100-4]
• 18: LAMBEK, J. 1989. Multicategories revisited. In Contemporary Mathematics, vol. 92. J. W. Gray and A. Scedrov, eds. American Mathematical Society, Providence, R.I., pp. 217-240.
• 19: LENT, A.F. 1993. The category of functors from state shapes to bottomless CPOs is adequate for block structure. In Proceedings of the ACM SPGPLAN Workshop on State in Programming Languages (Copenhagen, Denmark, June 12, 1993). ACM, New York, pp. 101-119.
• 20: MACKIE, I. 1994. Lilac: A functional programming language based on linear logic. J. Funct. Prog. 4, 4 (Oct.), 395-433.
• 21: MILNER, R. 1977. Fully abstract models of typed A-calculi. Theoret. Comput. Sci. 4, 1-22.
• 22: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 23: P. W. O'Hearn , A. J. Power , M. Takeyama , R. D. Tennent, Syntactic control of interference revisited, Theoretical Computer Science, v.228 n.1-2, p.211-252, Oct. 1999 [doi>10.1016/S0304-3975(98)00359-4]
• 24: Peter W. O'Hearn , Uday S. Reddy, Objects, interference, and the Yoneda embedding, Theoretical Computer Science, v.228 n.1-2, p.253-282, Oct. 1999 [doi>10.1016/S0304-3975(98)00360-0]
• 25: Peter W. O'Hearn , Jon G. Riecke, Kripke logical relations and PCF, Information and Computation, v.120 n.1, p.107-116, July 1995 [doi>10.1006/inco.1995.1103]
• 26: P. W. O'Hearn , R. D. Tennent, Parametricity and local variables, Journal of the ACM (JACM), v.42 n.3, p.658-709, May 1995 [doi>10.1145/210346.210425]
• 27: Peter O'Hearn , Robert D. Tennent, ALGOL-like languages (v.2), Birkhauser Boston Inc., Cambridge, MA, 1996
• 28: Peter O'Hearn , Robert D. Tennent, ALGOL-like languages (v.2), Birkhauser Boston Inc., Cambridge, MA, 1996
• 29: Frank Joseph Oles, A category-theoretic approach to the semantics of programming languages, 1982
• 30: OLES, F. J. 1987. Lambda calculi with implicit type conversions. Tech.Rep. RC 13245. IBM Research, T. J. Watson Research Center, Yorktown Heights, N.Y.
• 31: OLES, F. J. 1997. Functor categories and store shapes. In Algol-like Languages, Vol. 2. P. W. O'Hearn and R. D. Tennent, eds. Birkhauser, Boston, Mass., pp. 3-12.
• 32: PITTS, A. 1997. Reasoning about local variables with operationally-based logical relations. In Algol-like Languages, vol. 2. P. W. O'Hearn and R. D. Tennent, eds. Birkhauser, Boston, Mass., pp. 165-186.
• 33: PLOTKIN, G. D. 1977. LCF considered as a programming language. Theoret. Comput. Sci. 5, 223-255.
• 34: PLOTKIN, G.D. 1980. Lambda-definability in the full type hierarchy. In To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley, eds. Academic Press, Orlando, Fla., pp. 353-373.
• 35: PLOTKIN, G. 1983. Domains. 1992 TeXed edition of course notes prepared by Yugo Kashiwagi and Hidetaka Kondoh from notes by Tatsuya Hagino.
• 36: PLOTKIN, G. D. 1993. Type theory and recursion (extended abstract). In Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science (Montreal, Ont., Canada, June 19-23). IEEE Computer Society Press, Los Alamitos, Calif., page 374.
• 37: Gordon D. Plotkin , Martín Abadi, A Logic for Parametric Polymorphism, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.361-375, March 16-18, 1993
• 38: REDDY, U.S. 1996. Global states considered unnecessary: introduction to object-based semantics. Lisp and Symbolic Computation. Special issue on State in Programming Languages. Also in O'Hearn and Tennent 1997b}, pages 227-296.
• 39: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 40: John C. Reynolds, Syntactic control of interference, ALGOL-like Languages, Volume 1, Birkhauser Boston Inc., Cambridge, MA, 1997
• 41: John C. Reynolds, The Craft of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 42: John C. Reynolds, The essence of ALGOL, ALGOL-like Languages, Volume 1, Birkhauser Boston Inc., Cambridge, MA, 1997
• 43: REYNOLDS, J.C. 1983. Types, abstraction and parametric polymorphism. In Information Processing, vol. 83, R. E. A. Mason, ed. North-Holland, Amsterdam, pp. 513-523.
• 44: Jon G. Riecke , Anders Sandholm, A Relational Account of Call-by-Value Sequentially, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.258, June 29-July 02, 1997
• 45: David A. Schmidt, Detecting global variables in denotational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.2, p.299-310, April 1985 [doi>10.1145/3318.3323]
• 46: SCOTT, D.S. 1972. Mathematical concepts in programming language semantics. In Proceedings of the 1972 Spring Joint Computer Conference, AFIPS Press, Montvale, N.J., pp. 225-234.
• 47: SCOTT, D. S., AND STRACHEY, C. 1971. Toward a mathematical semantics for computer languages. In Proceedings of the Symposium on Computers and Automata, Volume 21 of Microwave Research Institute Symposia Series, Polytechnic Institute of Brooklyn Press, Brooklyn, N.Y., pp. 19-46.
• 48: Kurt Sieber, Full abstraction for the second order subset of an ALGOL-like language, Theoretical Computer Science, v.168 n.1, p.155-212, Nov. 10, 1996
• 49: Christopher Strachey, The varieties of programming language, ALGOL-like Languages, Volume 1, Birkhauser Boston Inc., Cambridge, MA, 1997
• 50: R. D. Tennent, Principles of Programming Languages, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 51: WADLER, P. 1990. Linear types can change the world! In IFIP TC-2 Working Conference on Programming Concepts and Methods, M. Broy and C. Jones, eds. (Sea of Galilee, Israel, Apr.). North-Holland, Amsterdam, The Netherlands, pp. 347-359.
• 52: Philip Wadler, Is there a use for linear logic?, Proceedings of the 1991 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.255-273, June 17-19, 1991, New Haven, Connecticut, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

General Terms:
Languages, Theory

Keywords:
linear logic, local state, logical relations, parametric polymorphism