Formal Program Verification and Computabitity Theory
Document Type
Conference Proceeding
Publication Date
4-8-1992
Description
Whereas early researchers in computability theory described effective computability in terms of such models as Turing machines, Markov algorithms, and register machines, a recent trend has been to use simple programming languages as computability models. A parallel development to this programming approach to computability theory is the current interest in systematic and scientific development and proof of programs. This paper investigates the feasibility of using formal proofs of programs in computability theory. After describing a framework for formal verification of programs written in a simple theoretical programming language, we discuss the proofs of several typical programs used in computability theory.
Citation Information
Shah, Paresh B.; and Pleasant, James C.. 1992. Formal Program Verification and Computabitity Theory. Proceedings of the 30th Annual Southeast Regional Conference, ACM-SE 1992. 471-473. https://doi.org/10.1145/503720.503809 ISBN: 0897915062,9780897915069