Gordon, Michael J. C.

2013-04-05T14:07:27Z

2013-04-05T14:07:27Z

1973

A Scott/Strachey style denotational semantics intended to describe pure LISP is examined. I present evidence that it is an accurate rendering of the language described in chapter 1 of the LISP 1.5 Programmer's, Manual, in particular I show that call-by-value and fluid variables are correctly handled. To do this I have: (1) written an operational 'semantics' of pure LISP and shown it equivalent to the denotational one (2) Proved that, relative to the denotational semantics, the LISP functions apply,eval,...,etc. correctly compute meanings. The proof techniques used are derived from the work of Wadsworth; roughly one first proves the results for a class of 'finite' programs and then extends them to all programs by a limiting argument. Conceptually these arguments are inductions on length of computation and to bring this out I've formulated a rule of inference which enables such operational reasoning to be applied to the denotational semantics.

http://hdl.handle.net/1842/6654

en

The University of Edinburgh

Gordon, M.J.C. An investigation of lit: where lit((A1...A n ),A n+1,f)=f(A1,f(A 21?...,f(A n A n+1 ))). Research Memorandum IMP--R-101. Edinburgh: School of Artificial Intelligence, University of Edinburgh. (1973).

Computer program language

LISP

Programming languages

Evaluation and denotation of pure LISP programs: a worked example in semantics

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy