Abstract
Variants of the λ-calculus together with D. Scott’s lattice-theoretic models have turned out to be a basic tool for describing the semantics of programming languages (e.g. [LANDIN 66], [REYNOLDS 72, 74], [SCOTT 74], [SCOTT-STRACHEY 71]). Based upon these approaches, in LCF [WEYHRAUCH-MILNER 72] a typed λ-calculus has been imbedded into a type theory providing a system in which properties about programs can be proven and programs can be constructed according to the properties being specified. The D-calculus presented in this paper contains essentially three new concepts that extend and refine the above systems:
-
(1)
The D-calculus is an overtyped system combining the advantages of both typed and untyped systems without having the restrictions brought about by types. Hence, e.g. the semantics of programming language constructs having side effects and procedures taking arbitrary procedures as arguments as well as the intricacies of modes in ALGOL 68 can be adequately described in overtyped systems. A detailed account of overtyping the λ-calculus and such examples of applications is given in [RAULEFS 74].
-
(2)
Abstract data types are introduced in terms of inverse systems of complete partially ordered sets (cpo-sets) that are refinements of the lattices developed by Scott and reflect the structure of data types more closely.
-
(3)
The β-reduction mechanism of the λ-calculus is generalized to matching the binder to the argument — i.e. computing a substitution that makes the binder equal to the argument — and applying this substitution to the body of the λ-term. The control structure of “sugared” λ-calculi is generalized by using a pattern matching mechanism.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Landin, P. A λ-calculus approach. In Advances in Programming and Non-Numerical Computation, L. Fox (ed.), Pergamon Press, 1966: 97–141.
Raulefs, P. The overtyped A-calculus and its application for describing semantics of programming languages. Technical Report, Inst. f. Informatik I, Karlsruhe Univ., Nov. 1974.
Raulefs, P. Dissertation, 1975
Reynolds, J.C. Definitional interpreters for higer-order programming languages. Proc. ACM 1972 Ann. Conf.: 717–740
Reynolds, J.C. Notes on a lattice-theoretic approach to the theory of computation. Tech. Rep., Systems and Information Science Dept., Syracuse University, 1972.
Reynolds, J.C. On the relation between direct and continuation semantics. Proc. 2nd Coll. on Automata, Languages and Programming 1974 (ed. J. Loeckx), Springer Lecture Notes in Computer Science vol. 14 (1974): 141–156.
Scott, D. Data types as lattices. Mimeographed notes, Kiel International Summer School and Logic Conference, 1974.
Scott, D. and C. Strachey. Towards a mathematical semantics for computer languages. Proc. Symp. Computer and Automata, Polytechnic Inst. of Brooklyn, 1971: 19–46.
Tennent, R.D. Mathematical semantics of SNOBOL4. Proc. ACM Symp. Principles of Programming Languages, Boston, Oct. 1973: 95–107.
Weyhrauch, R. and R. Milner. Program semantics and correctness in a mechanized logic. Proc. 1st USA-.Japan Comp. Conf., 1972: 384–392.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1975 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Raulefs, P. (1975). The D-Calculus: A System to Describe the Semantics of Programs Involving Complex Data Types. In: Siefkes, D. (eds) GI-4.Jahrestagung. Lecture Notes in Computer Science, vol 26. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-40087-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-662-40087-6_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-39104-4
Online ISBN: 978-3-662-40087-6
eBook Packages: Springer Book Archive