*Result*: Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
Title:
Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
Authors:
Contributors:
The Pennsylvania State University CiteSeerX Archives
Collection:
CiteSeerX
Subject Terms:
Document Type:
*Academic Journal*
text
File Description:
application/pdf
Language:
English
Availability:
Rights:
Metadata may be used without restrictions as long as the oai identifier remains attached to it.
Accession Number:
edsbas.77AFA28C
Database:
BASE
*Further Information*
*In this paper we sketch an ACL2-checked proof that a simple but unbounded Von Neumann machine model is Turing Complete, i.e., can do anything a Turing machine can do. The project formally revisits the roots of computer science. It requires re-familiarizing oneself with the definitive model of computation from the 1930s, dealing with a simple “modern ” machine model, thinking carefully about the formal statement of an important theorem and the specification of both total and partial programs, writing a verifying compiler, including implementing an X86-like call/return protocol and implementing computed jumps, codifying a code proof strategy, and a little “creative ” reasoning about the non-termination of two machines.*