Embedding type structure in semantics

ABSTRACT

We show how a programming language designer may embed the type structure of a programming language in the more robust type structure of the typed lambda calculus. This is done by translating programs of the language into terms of the typed lambda calculus. Our translation, however, does not always yield a well-typed lambda term. Programs whose translations are not well-typed are considered meaningless, that is, ill-typed. We give a conditionally type-correct semantics for a simple language with continuation semantics. We provide a set of static type-checking rules for our source language, and prove that they are sound and complete: that is, a program passes the typing rules if and only if its translation is well-typed. This proves the correctness of our static semantics relative to the well-established typing rules of the typed lambda-calculus.

REFERENCES

• 1: [Clinger, Friedman, and Wand 82] Clinger, W., Friedman, D. P., and Wand, M. "A Scheme for a Higher-Level Semantic Algebra," presentation at US-French Seminar on the Application of Algebra to Language Definition and Compilation, Fontainebleau, France, 1982; proceedings to appear.
• 2: Robert L. Constable , Daniel R. Zlatin, The Type Theory of PL/CV3, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.94-117, Jan. 1984 [doi>10.1145/357233.357238]
• 3: [COPPO 84] Coppo, M. "Completeness of Type Assignment in Continuous Lambda Models" Theoret. Comp. Sci. 29 (1984) 309-324.
• 4: Steven Fortune , Daniel Leivant , Michael O'Donnell, The Expressiveness of Simple and Second-Order Type Structures, Journal of the ACM (JACM), v.30 n.1, p.151-185, Jan. 1983 [doi>10.1145/322358.322370]
• 5: [Friedman et al. 84] Friedman, D. P., Haynes, C. T., Kohlbecker, E., and Wand, M. "The Scheme 84 Reference Manual" Indiana University Computer Science Department Technical Report No. 153 (March, 1984).
• 6: Daniel P. Friedman , Christopher T. Haynes, Constraining control, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.245-254, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318654]
• 7: Michael J. C. Gordon, The Denotational Description of Programming Languages: An Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 8: [Hindley 69] Hindley, R. "The Principal Type-Scheme of an Object in Combinatory Logic," Trans. Am. Math. Soc. 146 (1969) 29-60.
• 9: [Hindley 83a] Hindley, R. "The Completeness Theorem for Typing ¿-Terms" Theoret. Comp. Sci. 22 (1983) 1-17.
• 10: [Hindley 83b] Hindley, R. "Curry's Type-rules are Complete with Respect to the F-Semantics Too" Theoret. Comp. Sci. 22 (1983) 127-133.
• 11: James G. Hook, Understanding Russell–a first attempt, Proc. of the international symposium on Semantics of data types, p.69-85, July 1984, Sophia-Antipolis, France
• 12: [Kahn, MacQueen, & Plotkin 84] Kahn, G., MacQueen, D. B., & Plotkin, G. D., (Eds.) Semantics of Data Types: Proceedings, Lecture Notes in Computer Science, Volume 173, Springer-Verlag, 1984.
• 13: [Martin-Löf 79] Martin-Löf, P. "Constructive Mathematics and Computer Programming," Proc. 6th Intl. Congress for Logic, Methodology, and Philosophy of Science, (Hannover, August, 1979).
• 14: Robert Milne , C. Strachey, A Theory of Programming Language Semantics, Halsted Press, New York, NY, 1977
• 15: [Milner 78] Milner, R. "A Theory of Type Polymorphism in Programming," J. Comp. & Sys. Sci. 17 (1978), 348-375.
• 16: [Strachey 73] Strachey, C. "The Varieties of Programming Language," Oxford University Computing Laboratory, Technical Monograph PRG-10 (1973).
• 17: Mitchell Wand, Deriving Target Code as a Representation of Continuation Semantics, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.496-517, July 1982 [doi>10.1145/357172.357179]
• 18: Mitchell Wand, A types-as-sets semantics for milner-style polymorphism, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.158-164, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800527]

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.3 Studies of Program Constructs
          Subjects: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Design, Languages, Performance, Theory, Verification