Fixpoint approach to the theory of computation
- 1 July 1972
- journal article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 15 (7), 528-536
- https://doi.org/10.1145/361454.361460
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.Keywords
This publication has 11 references indexed in Scilit:
- Implementation and applications of Scott's logic for computable functionsPublished by Association for Computing Machinery (ACM) ,1972
- Another recursion induction principleCommunications of the ACM, 1971
- Procedures and parameters: An axiomatic approachLecture Notes in Mathematics, 1971
- Formalization of Properties of Functional ProgramsJournal of the ACM, 1970
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- Proving Properties of Programs by Structural InductionThe Computer Journal, 1969
- Letters to the editor: go to statement considered harmfulCommunications of the ACM, 1968
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967
- Proof of algorithms by general snapshotsBIT Numerical Mathematics, 1966
- Correspondence between ALGOL 60 and Church's Lambda-notationCommunications of the ACM, 1965