Show simple item record

dc.contributor.authorGordon, Michael J. C.en
dc.date.accessioned2013-04-05T14:07:27Z
dc.date.available2013-04-05T14:07:27Z
dc.date.issued1973
dc.identifier.urihttp://hdl.handle.net/1842/6654
dc.description.abstractA 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.en
dc.language.isoen
dc.publisherThe University of Edinburghen
dc.relation.hasversionGordon, 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).en
dc.subjectComputer program languageen
dc.subjectLISPen
dc.subjectProgramming languagesen
dc.titleEvaluation and denotation of pure LISP programs: a worked example in semanticsen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record