×

Proving a compiler correct: A simple approach. (English) Zbl 0304.68022


MSC:

68N01 General topics in the theory of software
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Blum, E. K., Towards a theory of semantics and compilers for programming languages, J. Comput. System Sci., 3, 248-275 (1969) · Zbl 0174.28903
[2] Dijkstra, E. W., GO TO statements considered harmful, Comm. ACM., 11, 147-148 (1968)
[3] Eilenberg, S.; Elgot, C. C., Recursiveness (1970), Academic Press: Academic Press New York · Zbl 0211.31101
[4] Germano, G.; Maggiolo-Schettini, A., Eliminability of concluding formulas in Markov’s normal algorithms, Notices Amer. Math. Soc., 18, 426 (1971)
[5] Germano, G.; Maggiolo-Schettini, A., Eliminability of concluding formulas in Markov’s normal algorithms II, Notices Amer. Math. Soc., 18, 660 (1971)
[6] Germano, G.; Maggiolo-Schettini, A., Markov’s normal algorithms without concluding formulas: an application, (IVth International Congress for Logic, Methodology and Philosophy of Science, Centre of Information and Documentation in Social and Political Sciences. IVth International Congress for Logic, Methodology and Philosophy of Science, Centre of Information and Documentation in Social and Political Sciences, Bucharest 6 (August 29-September 4, 1971)) · Zbl 0283.68026
[7] Germano, G.; Maggiolo-Schettini, A., Equivalence of partial recursivity and computability by algorithms without concluding formulas, Calcolo, 8, 273-292 (1971) · Zbl 0242.02043
[8] Germano, G.; Maggiolo-Schettini, A., A Characterization of partial recursive functions via sequence functions, Notices Amer. Math. Soc., 19, 332 (1972) · Zbl 0242.02043
[9] Germano, G., A new theory of calculability, (Seminaires IRIA: Théorie des Algorithmes, des Languages et de la Programmation. Seminaires IRIA: Théorie des Algorithmes, des Languages et de la Programmation, IRIA, Rocquencourt, 78150 Le Chesnay, France (1972)), 33-36
[10] Germano, G.; Maggiolo-Schettini, A., Quelques caractérisations des fonctions récursives partielles, C. R. Acad. Sci. Paris, 276, 1325-1327 (1973) · Zbl 0324.02025
[11] Germano, G.; Maggiolo-Schettini, A., A flow diagram composition of Markov’s normal algorithms without concluding formulas, BIT, 13, 301-312 (1973) · Zbl 0283.68026
[12] Germano, G.; Maggiolo-Schettini, A., Recursivity and models of programs, (Report LC 116 (April 1973), Laboratorio di Cibernetica: Laboratorio di Cibernetica 80072 Arco Felice, Italy) · Zbl 0339.68003
[13] Germano, G.; Maggiolo-Schettini, A., Sequence-to-sequence recursive functions: a systematic study, (Report RC 5108 (October 1974), IBM T. J. Watson Research Center: IBM T. J. Watson Research Center Yorktown Heights, NY 10598) · Zbl 0311.02047
[14] Germano, G.; Maggiolo-Schettini, A., A language for Markov’s algorithms composition, (Report LC 214 (December 1973), Laboratorio di Cibernetica: Laboratorio di Cibernetica 80072 Arco Felice, Italy) · Zbl 0345.02021
[15] Knuth, D. E., Semantics of context-free languages, Math. Systems Theory, 2, 127-145 (1968) · Zbl 0169.01401
[16] London, R. L., Correctness of a compiler for a LISP subset, (Proceedings of an ACM Conference on Proving Assertions about Programs. Proceedings of an ACM Conference on Proving Assertions about Programs, Las Cruces, New Mexico (January 6-7, 1972)), 121-125
[17] Lucas, P.; Lauer, P.; Stigleitner, H., Method and notation for the formal definition of programming languages, (Technical Report TR 25.087 (June 1968), IBM Laboratory: IBM Laboratory Vienna)
[20] Morris, F. L., Advice on structuring compilers and proving them correct, (Conference Record of an ACM Symposium on Principles of Programming Languages. Conference Record of an ACM Symposium on Principles of Programming Languages, Boston, MA (October 1-3, 1973)), 144-152 · Zbl 0309.68026
[21] Scott, D.; Strachey, C., Towards a mathematical semantics for computer languages, (Technical Monograph PRG-6 (August 1971), Oxford University Computing Laboratory, Programming Research Group) · Zbl 0268.68004
[22] Wegner, P., Operational semantics of programming languages, (Proceedings of an ACM Conference on Proving Assertions about Programs. Proceedings of an ACM Conference on Proving Assertions about Programs, Las Cruces, New Mexico (January 6-7, 1972)), 128-141
[24] Wulf, W. A., A Case against GO TO, (Proceedings of the ACM Annual Conference. Proceedings of the ACM Annual Conference, Boston (August, 1972)), 791-797
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.