ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
Advice on structuring compilers and proving them correct
Full text PdfPdf (674 KB)
Source Annual Symposium on Principles of Programming Languages archive
Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages table of contents
Boston, Massachusetts
Pages: 144 - 152  
Year of Publication: 1973
Author
F. Lockwood Morris  Syracuse University
Sponsors
SIGPLAN: ACM Special Interest Group on Programming Languages
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 9,   Downloads (12 Months): 38,   Citation Count: 27
Additional Information:

abstract   references   cited by   collaborative colleagues  

Tools and Actions: Request Permissions Request Permissions    Review this Article  
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/512927.512941
What is a DOI?

ABSTRACT

The purpose of this paper is to advise an approach (and to support that advice by discussion of an example) towards achieving a goal first announced by John McCarthy: that compilers for higher-level programming languages should be made completely trustworthy by proving their correctness. The author believes that the compiler-correctness problem can be made much less general and better-structured than the unrestricted program-correctness problem; to do so will of course entail restricting what a compiler may be.


REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

 
1
G. Birkhoff and J. D. Lipson, "Heterogeneous Algebras", J. Combinatorial Theory 8, pp. 115-133 (1970).
 
2
R. M. Burstall and P. J. Landin, "Programs and Their Proofs: an Algebraic Approach", Machine Intelligence 4 (1969).
 
3
D. Scott and C. Strachey, "Towards a Mathematical Semantics for Computer Languages", Programming Research Group Monograph PRG-6, Oxford Computing Laboratory (1971).
 
4
P. J. Landin, "A Program-Machine Symmetric Automata Theory", Machine Intelligence 5 (1970).
 
5
F. L. Morris, "Correctness of Translations of Programming Languages", Stanford Computer Science Memo CS 72-303 (1972).
 
6
R. Milner and R. Weyhrauch, "Proving Compiler Correctness in a Mechanized Logic", Machine Intelligence 7 (1972).
 
7
P. Hitchcock and D. Park, "Induction Rules and Proofs of Termination", Proc. Colloques IRIA Theorie des automates des langages et de la Programmation. Rocquencourt, France, July 1972.

CITED BY  27
Ravi Sethi, Control flow aspects of semantics directed compiling (Summary), ACM SIGPLAN Notices, v.17 n.6, p.245-260, June 1982
J. A. Goguen , J. W. Thatcher , E. G. Wagner , J. B. Wright, Initial Algebra Semantics and Continuous Algebras, Journal of the ACM (JACM), v.24 n.1, p.68-95, Jan. 1977
Torben Poort Lange, The correctness of an optimized code generation, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.167-178, June 14-16, 1993, Copenhagen, Denmark
Mitchell Wand, Semantics-directed machine architecture, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.234-241, January 25-27, 1982, Albuquerque, Mexico
J. Craig Cleaveland, Programming languages considered as abstract data types, Proceedings of the ACM 1980 annual conference, p.236-245, January 1980
Ravi Sethi, Control Flow Aspects of Semantics-Directed Compiling, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.4, p.554-595, Oct. 1983
Jean-Claude Raoult , Ravi Sethi, Properties of a Notation for Combining Functions, Journal of the ACM (JACM), v.30 n.3, p.595-611, July 1983
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
Harald Ganzinger , Robert Giegerich, Attribute coupled grammars, ACM SIGPLAN Notices, v.19 n.6, p.157-170, June 1984
Wan Fokkink , Jasper Kamperman , Pum Walters, Within ARM's reach: compilation of left-linear rewrite systems via minimal rewrite systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.3, p.679-706, May 1998
Teodor Rus , Eric Van Wyk , Tom Halverson, Generating Model Checkers from Algebraic Specifications, Formal Methods in System Design, v.20 n.3, p.249-284, May 2002
Veronique Royer, Transformations of denotational semantics in semantics directed compiler generation, ACM SIGPLAN Notices, v.21 n.7, p.68-73, July 1986
William Clinger, The scheme 311 compiler an exercise in denotational semantics, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.356-364, August 06-08, 1984, Austin, Texas, United States
Robert van Engelen , David Whalley , Xin Yuan, Validation of code-improving transformations for embeded systems, Proceedings of the 2003 ACM symposium on Applied computing, March 09-12, 2003, Melbourne, Florida
Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States
E. Gansner , J. R. Horgan , C. M. R. Kintala , D. J. Moore , P. Surko, Semantics and correctness of a query language translation: (preliminary version), Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.289-298, January 25-27, 1982, Albuquerque, Mexico
Sorin Lerner , Todd Millstein , Craig Chambers, Automatically proving the correctness of compiler optimizations, ACM SIGPLAN Notices, v.38 n.5, May 2003
Maulik A. Dave, Compiler verification: a bibliography, ACM SIGSOFT Software Engineering Notes, v.28 n.6, November 2003
Laurian M. Chirica , David F. Martin, Toward compiler implementation correctness proofs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.185-214, April 1986
George C. Necula, Translation validation for an optimizing compiler, ACM SIGPLAN Notices, v.35 n.5, p.83-94, May 2000
George C. Necula , Peter Lee, The design and implementation of a certifying compiler, ACM SIGPLAN Notices, v.33 n.5, p.333-344, May 1998
Fernando Orejas, Even more on advice on structuring compilers and proving them correct: changing an arrow, ACM SIGPLAN Notices, v.16 n.3, p.82-84, March 1981
Robert van Engelen , David Whalley , Xin Yuan, Automatic validation of code-improving transformations on low-level program representations, Science of Computer Programming, v.52 n.1-3, p.257-280, August 2004
Cliff B. Jones, The Early Search for Tractable Ways of Reasoning about Programs, IEEE Annals of the History of Computing, v.25 n.2, p.26-49, April 2003
Eric Van Wyk, Specification languages in algebraic compilers, Theoretical Computer Science, v.291 n.3, p.351-385, 6 January 2003
Claude Kirchner , Pierre-Etienne Moreau , Antoine Reilles, Formal validation of pattern matching code, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.187-197, July 11-13, 2005, Lisbon, Portugal
George C. Necula , Peter Lee, The design and implementation of a certifying compiler, ACM SIGPLAN Notices, v.39 n.4, April 2004
Collaborative Colleagues:
F. Lockwood Morris: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player