A computer Proof of the Correctness of a Simple Optimizing Compiler for Expressions.

Abstract

This paper presents an automatic computer proof of the correctness of a simple optimizing compiler for expressions. The proof was produced by a new theorem prover, resembling the Boyer-Moore Pure LISP Theorem Prover but operating on a much richer domain of functions and objects.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1977
Accession Number
ADA036121

Entities

People

  • J. Strother Moore
  • Robert S. Boyer

Organizations

  • SRI International

Tags

DTIC Thesaurus Topics

  • Automatic
  • Compilers
  • Computer Language Translators
  • Computer Programs
  • Computers
  • Computing Devices

Fields of Study

  • Computer science

Readers

  • Computational Linguistics