Abstract
Imperative lambda calculus (ILC) is an abstract formal language obtained by extending the typed lambda calculus with imperative programming features, namely references and assignments. The language shares with typed lambda calculus important properties such as the Church-Rosser property and strong normalization. In this paper, we describe the logical symmetries that underlie ILC by exhibiting a constructive logic for which ILC forms the language of constructions. Central to this formulation is the view that references play a role similar to that of variables. References can be used to range over values and instantiated to specific values. Thus, we obtain a new form of universal quantification that uses references instead of variables. The essential term forms of ILC are then obtained as the constructions for the introduction and elimination of this quantifier. While references duplicate the role of variables, they also have important differences. References are semantic values whereas variables are syntactic entities and, secondly, references are reusable. These differences allow references to be used in a more flexible fashion leading to efficiency in constructions and algorithms.
Supported by NASA grant NAG-1-613 (while at the University of Illinois at Urbana-Champaign).
Supported by a grant from Motorola Corporation.
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky. Computational interpretations of linear logic. Research Report DOC 90/20, Imperial College, London, Oct 1990.
H. B. Curry and R. Feys. Combinatory Logic. North-Holland, Amsterdam, 1958.
R. L. Constable, et. al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, New York, 1986.
E. Engeler. Algorithmic logic. In J. W. de Bakker, editor, Foundations of Computer Science, pages 57–85. Mathematisch Centrum, Amsterdam, 1975. (Mathematical Centre Tracts 63).
J.-Y. Girard. Linear logic. Theoretical Comp. Science, 50:1–102, 1987.
H. H. Goldstine and J. von Neumann. Planning and coding problems for an electronic computing instrument, Part II. In John von Neumann, Collected Works, Vol. V, pages 80–151. Pergamon Press, 1963, Oxford, 1947.
C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576–583, 1969.
W. A. Howard. The formulae-as-types notion of construction. In J. R. Hindley and J. P. Seldin, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, New York, 1980.
P. Hudak and P. Wadler (eds). Report on programming language Haskell, A non-strict purely functional language (Version 1.0). Technical Report YALEU/DCS/RR777, Yale University, Apr 1990.
G. Lindstrom. Functional programming and the logical variable. In ACM Symp. on Princ. of Program. Languages, 1985.
P. Martin-Löf. Constructive mathematics and computer programming. In L. J. Cohen, J. Los, H. Pfeiffer, and K.-P. Podewski, editors, Proc. Sixth Intern. Congress for Logic, Methodology and Philosophy of Science, pages 153–175, Amsterdam, 1982. North-Holland.
Per Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, Napoli, 1984.
G. Mirkowska and A. Salwicki. Algorithmic Logic. PWN — Polish Scientific Publishers, Warzwawa, Poland, 1987.
V. Pratt. Semantic considerations on Floyd-Hoare logic. In Symp. on Foundations of Computer Science, pages 109–121. IEEE, 1976.
J. C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages, pages 345–372. North-Holland, 1981.
J. C. Reynolds. Idealized Algol and its specification logic. In D. Neel, editor, Tools and Notions for Program Construction, pages 121–161. Cambridge Univ. Press, 1982.
V. Swarup, U. S. Reddy, and E. Ireland. Assignments for applicative languages. In R. J. M. Hughes, editor, Conf. on Functional Program. Lang. and Comput. Arch. Springer-Verlag, Berlin, 1991. (Earlier versions: University of Illinois at Urbana-Champaign, July 1990, Revised Nov 1990, Feb 1991).
V. Swarup. Type Theoretic Properties of Assignments. PhD thesis, Univ. Illinois at Urbana-Champaign, 1991. (to appear).
R. D. Tennent. Denotational semantics of Algol-like languages. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Vol II. Oxford University Press, 1989. (to appear).
D. H. D. Warren, L. M. Pereira, and F. Pereira. Prolog — the language and its implementation compared with Lisp. SIGPLAN Notices, 12(8), 1977.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Swarup, V., Reddy, U.S. (1992). A logical view of assignments. In: Myers, J.P., O'Donnell, M.J. (eds) Constructivity in Computer Science. Constructivity in CS 1991. Lecture Notes in Computer Science, vol 613. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0021087
Download citation
DOI: https://doi.org/10.1007/BFb0021087
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55631-2
Online ISBN: 978-3-540-47265-0
eBook Packages: Springer Book Archive