Experience with an experimental compiler generator based on denotational semantics

ABSTRACT

Compiler generation based on formal semantics has received considerable attention in recent years from a number of semanticists. Compiler writers, on the other hand, know relatively little about these efforts. This paper tries to remedy this situation by discussing our experimentation with the Semantics Implementation System (SIS) of Peter Mosses. SIS allows the user to generate a complete compiler from a formal specification of the syntax and semantics of a programming language. In particular, the translator component of a compiler is obtained by directly implementing a denotational semantics. Consequently, a compiler is expressed as a higher order function. A program is compiled by formally applying the compiler to a tree representation of the program and simplifying this application. The experimentation with SIS indicates that compiler generation based on denotational semantics is feasible, though not yet viable. We argue that SIS constitutes an important first step toward the automatic construction of provably correct, complete, and reasonably efficient compilers from formal syntactic and semantic specifications.

REFERENCES

• 1: Donzeau-Gouge, V., Kahn, G., and Lang, B. A Complete Machine-Checked Definition of a Simple Programming Language Using Denotational Semantics. IRIA Rapport de Recherche No. 330, Le Chesnay, France, October 1978.
• 2: Marie-Claude Gaudel, Compiler Generation from Formal Definition of Programming Languages: A Survey, Proceedings of the International Colloquium on Formalization of Programming Concepts, p.96-114, April 19-25, 1981
• 3: Johnson, S.C. YACC: Yet Another Compiler-Compiler. Bell Laboratories Computing Science Technical Report No. 32, Murray Hill, NJ, 1975.
• 4: Neil D. Jones, Semantics-Directed Compiler Generation: Proceedings, Springer-Verlag New York, Inc., Secaucus, NJ, 1980
• 5: Jones, N.D., and Christiansen, H. Control Flow Treatment in a Simple Semantics-Directed Compiler Generator. DAIMI PB-137, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981.
• 6: Zohar Manna, Mathematical Theory of Computation, Dover Publications, Incorporated, 2003
• 7: Robert Milne , C. Strachey, A Theory of Programming Language Semantics, Halsted Press, New York, NY, 1977
• 8: Mosses, P.D. SIS—Semantics Implementation System (Reference Manual and User Guide). DIAMI MD-30, Computer Science Department, Aarhus University, Aarhus, Denmark, August 1979.
• 9: Mosses, P. SIS—Operating Notes. DAIMI MD-32, Computer Science Department, Aarhus University, Aarhus, Denmark, August 1979.
• 10: Mosses, P. SIS—Tested Examples. DAIMI MD-33, Computer Science Department, Aarhus University, Aarhus, Denmark, August 1979.
• 11: Mosses, P. SIS—A Brief Description of SIS. Supplied as part of the documentation.
• 12: Mosses, P. Abstract Semantic Algebras (Preliminary Version). DAIMI IR-29, Computer Science Department, Aarhus University, Aarhus, Denmark, October 1981.
• 13: Steven S. Muchnick , Uwe F. Pleban, A semantic comparison of LISP and SCHEME, Proceedings of the 1980 ACM conference on LISP and functional programming, p.56-64, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802790]
• 14: Muchnick, S.S., and Pleban, U.F. The Denotational Semantic Comparison of Programming Languages. Submitted to ACM TOPLAS.
• 15: Petersen, K.B. SIS—Implementation Notes. DAIMI MD-31, Computer Science Department, Aarhus University, Aarhus, Denmark, August 1979.
• 16: Scott, D.S. Data Types as Lattices. SIAM Journal of Computing 5, 1976, 522-587.
• 17: Martin R. Raskovsky , Philip A. Collier, From standard to implementation denotational semantics, Semantics-Directed Compiler Generation, Proceedings of a Workshop, p.94-139, January 14-18, 1980
• 18: Sethi, R. Control Flow Aspects of Semantics Directed Compiling. Computing Science Technical Report No. 98, Bell Laboratories, September 1981.
• 19: Guy L. Steele, Jr., Rabbit: A Compiler for Scheme, Massachusetts Institute of Technology, Cambridge, MA, 1978
• 20: Steele, G.L., Jr., and Sussman, G.J. The Revised Report on SCHEME, A Dialect of LISP. Memo 452, MIT AI Lab, January 1978.
• 21: R. D. Tennent, The denotational semantics of programming languages, Communications of the ACM, v.19 n.8, p.437-453, Aug. 1976 [doi>10.1145/360303.360308]
• 22: Tennent, R.D. A Denotational Definition of the Programming Language Pascal. Programming Research Group, University of Oxford, April, 1978.
• 23: Vuillemin, J.E. Correct and Optimal Implementations of Recursion in a Simple Programming Language. IRIA Rapport de Recherche No.24, Le Chesnay, France, 1973.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Translator writing systems and compiler generators

General Terms:
Experimentation, Languages