The Semantics of PASCAL in LCF

Abstract

The authors define a semantics for the arithmetic part of PASCAL by giving it an interpretation in LCF, a language based on the typed lambda- calculus. Programs are represented in terms of their abstract syntax. The authors show sample proofs, using LCF, of some general properties of PASCAL and the correctness of some particular programs. A program implementing the McCarthy Airline reservation system is proved correct.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1974
Accession Number
AD0787631

Entities

People

  • Luigia Aiello
  • Mario Aiello
  • Richard W. Weyhrauch

Organizations

  • Stanford University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Arithmetic
  • Artificial Intelligence
  • Automatic Programming
  • Computations
  • Computer Languages
  • Computer Programming
  • Computer Science
  • Computers
  • Instructions
  • Language
  • Programming Languages
  • Sequences
  • Side Effects
  • Standards
  • Theory Of Computation

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.