Accession Number : ADA130625

Title :   A Mechanical Proof of the Turing Completeness of Pure LISP.

Descriptive Note : Technical rept.,

Corporate Author : TEXAS UNIV AT AUSTIN INST FOR COMPUTING SCIENCE AND COMPUTER APPLICATIONS

Personal Author(s) : Boyer,Robert S ; Moore,J Strother

PDF Url : ADA130625

Report Date : May 1983

Pagination or Media Count : 39

Abstract : The authors describe a proof by a computer program of the Turing completeness of a computational paradigm akin to Pure LISP. That is, they define formally the notions of a Turing machine and of a version of Pure LISP and prove that anything that can be computed by a Turing machine can be computed by LISP. While this result is straightforward, they believe this is the first instance of a machine proving the Turing completeness of another computational paradigm. (Author)

Descriptors :   *Computer program verification, *Interpreters, Computer programming, Computations, Input, Output, Semantics, Theorems

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE