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. © 2014 Springer International Publishing.
CITATION STYLE
Moore, J. S. (2014). Proof pearl: Proving a simple von neumann machine turing complete. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8558 LNCS, pp. 406–420). Springer Verlag. https://doi.org/10.1007/978-3-319-08970-6_26
Mendeley helps you to discover research relevant for your work.