Accession Number:

ADA036121

Title:

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

Descriptive Note:

Technical rept.,

Corporate Author:

STANFORD RESEARCH INST MENLO PARK CALIF

Personal Author(s):

Report Date:

1977-01-01

Pagination or Media Count:

62.0

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE