Formal Sematics of LISP with Applications to Program Correctness

Abstract

Described are some experiments in the formalisation of the LISP programming language using LCF (Logic for Computable Functions). The bulk of each experiment was concerned with applying the formalisation to proofs of correctness of some interesting LISP functions using Milner's mechanised version of LCF.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1975
Accession Number
ADA005413

Entities

People

  • Marcolm C. Newey

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Artificial Intelligence
  • Central Processing Units
  • Computations
  • Computer Languages
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Formal Languages
  • Language
  • Linguistics
  • Lisp Programming Language
  • Machine Languages
  • Programming Languages
  • Recursive Functions
  • Theorems
  • Theses

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Systems Analysis and Design