BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-74-447
       ENTRY:: August 23, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: The semantics of PASCAL in LCF.
        TYPE:: Technical Report
      AUTHOR:: Aiello, Luigia
      AUTHOR:: Aiello, Mario
      AUTHOR:: Weyhrauch, Richard W.
        DATE:: August 1974
       PAGES:: 82
    ABSTRACT:: We 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. We 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.
       NOTES:: [Adminitrivia V1/Prg/19950823]
         END:: STAN//CS-TR-74-447