Correctness of Two Compilers for a Lisp Subset,

Abstract

Using mainly structural induction, proofs of correctness of each of two running Lisp compilers for the PDP-10 computer are given. Indluded are the rationale for presenting these proofs, a discussion of the proofs, and the changes needed to the second compiler to complete its proof. (Author)

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1971
Accession Number
AD0738568

Entities

People

  • Ralph L. London

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Applied Computer Science
  • Artificial Intelligence
  • Compilers
  • Computer Language Translators
  • Computer Programs
  • Computers

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Computer Science.
  • Theoretical Analysis.