More on advice on structuring compilers and proving them correct

  • James W. Thatcher
  • Eric G. Wagner
  • Jesse B. Wright
Compiling And Algebraic Semantics
Part of the Lecture Notes in Computer Science book series (LNCS, volume 94)


Flow Chart Target Language Operator Domain Algebraic Theory Source Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. (1975) (JAG, JWT, EGW, JBW) "Initial algebra semantics and continuous algebras," IBM Research Report RC-5701. November 1975. JACM 24 (1977) pp. 68–95.CrossRefGoogle Scholar
  2. (1976) (JWT, EGW, JBW) J. W. Thatcher, E. G. Wagner, and J. B. Wright "Specification of abstract data types using conditional axioms," IBM Research Report RC-6214, September 1976.Google Scholar
  3. (1976a) (JAG, JWT, EGW) J. A. Goguen J. W. Thatcher E. G. Wagner "An initial algebra approach to the specification, correctness, and implementation of abstract data types," IBM Research Report RC-6487, October 1976. To appear, Current Trends in Programming Methodology, IV: Data Structuring (R. Yeh, Ed.), pp. 80–149, Prentice Hall, New Jersey.Google Scholar
  4. (1976b) (EGW, JBW, JAG, JWT) E. G. Wagner, J. B. Wright, J. A. Goguen, and J. W. Thatcher "Some fundamentals of order algebraic semantics." Lecture Notes in Computer Science 45 (Mathematical Foundations of Computer Science 1976), Springer-Verlag, pp. 153–168; IBM Research Report RC 6020, May 1976.Google Scholar
  5. (1976c) "Rational algebraic theories and fixed-point solutions," Proceedings 17th IEEE Symposium on Foundations of Computing, Houston, Texas, October, 1976, pp. 147–158.Google Scholar
  6. (1977) (EGW, JWT, JBW) E. G. Wagner, J. W. Thatcher, J. B. Wright "Free continuous theories," IBM Research Report RC 6906, December, 1977. Accepted for publication, Fundamenta Informaticae.Google Scholar
  7. Arbib, M.A. and Giveon, Y. (1968) "Algebra automata I: Parallel programming as a prolegomena to the categorical approach," Information and Control 12 (1968) 331–345.Google Scholar
  8. Birkhoff, G. and Lipson, J.D. (1970) "Heterogeneous algebras," J. Combinatorial Theory 8 (1970) 115–133.Google Scholar
  9. Burstall, R.M. and Landin, P.J. (1969) "Programs and their proofs: an algebraic approach," Machine Intelligence 4, 1969.Google Scholar
  10. Elgot, C.C. (1973) "Monadic computation and iterative algebraic theories," IBM Research Report RC 4564, October 1973. Proceedings, Logic Colloquium 1973, North Holland (1975) 175–230.Google Scholar
  11. (1977) Elgot, C.C. "Some geometrical categories associated with flow chart schemes," IBM Research Report RC 6534, May 1977. Proceedings, Conference on Fundamentals of Computation Theory, Poznan-Kornik, Poland, 1977.Google Scholar
  12. Elgot, C.C. and Shepherdson, J.C. (1977) "A semantically meaningful characterization of reducible flow chart schemes," IBM Research Report RC 6656, July, 1977.Google Scholar
  13. Fiebrich, Rolf-Dieter (1978) "Generation of correct compiler parts from formal language descriptions," LRZ-Bericht Nr. 7802/1, Institut für Informatik der Ludwig-Maximilians-Universität, Müchen, 1978.Google Scholar
  14. Gaudel, M.C. (1980) "Specification of compilers as abstract data type representations," draft manuscript, IRIA, Paris France. Presented, Workshop on Semantics Directed Compiler Generation, Aarhus, Denmark, January 1980.Google Scholar
  15. (1980a) Gaudel, M.C. Thesis, March, 1980.Google Scholar
  16. Gremano, G. and Maggiolo-Schettini, A. (1975) "Proving a compiler correct: A simple approach," JCSS 10 (1975) 370–383.Google Scholar
  17. Guttag, J. V. (1975) "The specification and application to programming of abstract data types," Univ. of Toronto, Computer Systems Research Group, Technical Report CSRG-59, September, 1975.Google Scholar
  18. Lawvere, F.W. (1963) "Functorial semantics of algebraic theories," Proceedings, Nat'l Acad. Sci. 50 (1963) 869–872.Google Scholar
  19. McCarthy, J. and Painter, J. (1967) "Correctness of a compiler for arithmetic expressions," Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, Vol. 19 (J.T. Schwartz, Ed.) American Math. Soc., Providence R.I. (1967) 33–41.Google Scholar
  20. Milner, R. (1972) "Implementation and application of Scott's logic for computable functions," Proceedings, ACM Conference on Proving Assertions about Programs, Las Cruces, New Mexico, January, 1972, pp. 1–6.Google Scholar
  21. (1976) "Program semantics and mechanized proof," Mathematical Centre Tracts 82 (K.R. Apt and J.W. de Bakker (Eds.), Mathematisch Centrum, Amsterdam, 1976, pp. 3–44.Google Scholar
  22. Milner, R. and Weyrauch, R (1972) "Proving compiler correctness in a mechanized logic," Machine Intelligence 7 (B. Meltzer and D. Michie, Eds.), Edinburgh University Press (1972) 51–72.Google Scholar
  23. Morris, F. L. (1972) "Correctness of translations of programming languages," Stanford Computer Science Memo CS 72–303 (1972).Google Scholar
  24. (1973) Morris, F. L. "Advice on structuring compilers and proving them correct," Proceedings, ACM Symposium on Principles of Programming Languages, Boston (1973) 144–152.Google Scholar
  25. Mosses, P. (1977) "Making denotational semantics less concrete," manuscript, Aarhus University, August, 1977.Google Scholar
  26. (1978) Mosses, P. "Modular denotational semantics," Draft paper, 1978-11-11, Department of Computer Science, Institute of Mathematics, Aarhus University, 1978.Google Scholar
  27. (1979) Mosses, P. "A constructive approach to compiler correctness," draft manuscript, Department of Computer Science, Aarhus University, November 1979. Presented, Workshop on Semantics Directed Compiler Generation, Aarhus, January, 1980.Google Scholar
  28. Schmeck, Hartmut (1975) "Korrektheit von Übersetzungen," Bericht Nr. 3/75 des Institut für Infromatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel, 1975.Google Scholar
  29. Scott, D. and Strachey, C. (1971) "Toward a mathematical semantics for computer languages," Technical Monograph PRG-6, Oxford University Computing Laboratory, Programming Research Group, 1971.Google Scholar
  30. Zilles, S. N. (1974) "Algebraic specification of data types," Computation Structures Group Memo 119, MIT, Cambridge, Mass. (1974) 28–52.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1980

Authors and Affiliations

  • James W. Thatcher
    • 1
  • Eric G. Wagner
    • 1
  • Jesse B. Wright
    • 1
  1. 1.Mathematical Sciences DepartmentIBM Thomas J. Watson Research CenterYorktown HeightsUSA

Personalised recommendations