|
|
|---|
|
|
|
|---|
J S. Moore, “
Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete”
in G. Klein and R. Gamboa, editors, Interactive Theorem Proving, ITP
2014, Springer LNCS 8558, doi.org/10.1007/978-3-319-08970-6_26,
2014.
Relevance:M1 can compute anything a Turing machine
can. (The paper ought to be re-titled “Proving M1 Turing
Equivalent.”)
The “Simple Von Neumann machine” in question is M1. See the
ACL2 directory
Abstract
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.
See the ACL2 book