Fixpoint approach to the theory of computation

ABSTRACT

Following the fixpoint theory of Scott, the semantics of computer programs are defined in terms of the least fixpoints of recursive programs. This allows not only the justification of all existing verification techniques, but also their extension to the handling, in a uniform manner of various properties of computer programs, including correctness, termination, and equivalence.

REFERENCES

• 1: Ashcroft, E., and Manna, Z. (1971). The translation of "goto" programs to "while" programs. Proc. IFIP Cong. 1971.
• 2: Bekid, H. (1969). Definable operations in general algebra and the theory of automata and flowcharts. Unpublished memo, IBM, Vienna, Dec. 1969.
• 3: Burstall, R.M. (1969). Proving properties of programs by structural induction. Comput. J. 12, 1 (Feb. 1969), 41-48.
• 4: Jean-Marie Cadiou, Recursive definitions of partial functions and their computations, 1972
• 5: Cooper, D.C. (1971). Programs for mechanical program verification. In Machine Intelligence 6, B. Meltzer and D. Michie, (Eds.), Edinburgh University Press, 1971, pp. 43-59.
• 6: deBakker, J.W., and Scott, D. (1969). A theory of programs. Unpublished memo, Aug. 1969.
• 7: Edsger W. Dijkstra, Letters to the editor: go to statement considered harmful, Communications of the ACM, v.11 n.3, p.147-148, March 1968 [doi>10.1145/362929.362947]
• 8: Floyd, R.W. (1967). Assigning meanings to programs. In Proc. of a Symposium in Applied Mathematics, Vol. 19, Mathematical Aspects of Computer Science, J.T. Schwartz (Ed.), Amer. Math. Soc., pp. 19-32.
• 9: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 10: Hoare, C.A.R. (1971). Procedures and parameters: An axiomatic approach. In Symposium on Semantics of Algorithmic Languages, Lecture notes Mathematics, Vol. 188, E. Engelet (Ed.), Springer-Verlag, Berlin, pp. 102-116.
• 11: Kleene, S.C. (1952). Introduction to Meta-mathematics. Van Nostrand, Princeton, N.J., 1952.
• 12: Knuth, D.E., and Floyd, R.W. (1971). Notes on avoiding "goto" statements. Information Processing Letters 1 (Jan. 1971), 23-31.
• 13: P. J. Landin, Correspondence between ALGOL 60 and Church's Lambda-notation: part I, Communications of the ACM, v.8 n.2, p.89-101, Feb. 1965 [doi>10.1145/363744.363749]
• 14: Manna, Z. (1969). The correctness of programs. J. Computer & System Sciences 3, 2 (May 1969), 119-127.
• 15: Zohar Manna , Stephen Ness , Jean Vuillemin, Inductive methods for proving properties of programs, Proceedings of ACM conference on Proving assertions about programs, p.27-50, January 06-07, 1972, Las Cruces, New Mexico, United States
• 16: Zohar Manna , Amir Pnueli, Formalization of Properties of Functional Programs, Journal of the ACM (JACM), v.17 n.3, p.555-569, July 1970 [doi>10.1145/321592.321606]
• 17: McCarthy, J. (1963a). A basis for a mathematical theory of computation. In Computer Programming and Formal Systems, P. Braffort and D. Hirschberg (eds.), Humanities Press, New York, 1936, pp. 33-70.
• 18: McCarthy, J. (1963 b). Towards a mathematical science of computation. Proc. IFIP Cong. 1962, North Holland Pub. Co., Amsterdam, pp. 21-28.
• 19: Robin Milner, Implementation and applications of Scott's logic for computable functions, Proceedings of ACM conference on Proving assertions about programs, p.1-6, January 06-07, 1972, Las Cruces, New Mexico, United States
• 20: Morris, J. H. (1968). Lambda-calculus models for programming languages, Ph.D. Th., Project MAC, MAC-TR-57, MIT, Cambridge, Mass., Dec. 1968.
• 21: James H. Morris, Jr., Another recursion induction principle, Communications of the ACM, v.14 n.5, p.351-354, May 1971 [doi>10.1145/362588.362598]
• 22: Naur, P. (1966). Proof of algorithms by general snapshots, BIT 6 (1966), 310-316.
• 23: park, D. (1969). Fixpoint induction and proofs of program properties. In Machine Intelligence 5, B. Meltzer and D. Michie (Eds.), Edinburgh University Press, pp. 59-78.
• 24: Scott, D. (1970). Outline of a mathematical theory of computation. Oxford U. Computing Lab., Programming Res. Group, Tech. Mono. PRG-2, Oxford, England, Nov. 1970.
• 25: Scott, D., and Strachey, C. (1971).Towards a mathematical semantics for computer languages. Tech. Mono. PRG-6, Oxford U., Oxford, England, Aug. 1971.
• 26: Strachey, C. (1966). Towards a formal semantics. Proc. IFIP Working Conf. 1964, North-Holland Pub. Co., Amsterdam, pp. 198-220.
• 27: Jean Etienne Vuillemin, Proof-techniques for recursive programs., 1974
• 28: Weyhrauch, R., and Milner, R. (1972). Program semantics and correctness in a mechanized logic. The USA-Japan Computer Conf., Tokyo, Oct. 1972.

INDEX TERMS

Keywords:
computational induction, least fixpoints, recursive programs, semantics of programming languages, verification techniques