Stanford University. Libraries. Department of Special Collections and University Archives3840/2https://purl.stanford.edu/fr053by9154, Stanford University, Department of Computer Science, Technical Reports, and Stanford Artificial Intelligence Laboratory records, 1963-2009
PublishDate:
2021-02-05T23:21:04Z
Description:
"Obviously true" properties of programs can be hard to prove when meanings are specified with a denotational semantics. One cause of this is that such a semantics usually abstracts away from the running process - thus properties which are obvious when one thinks about this lose the basis of their obviousness in the absence of it. To enable process-based intuitions to be used in constructing proofs one can associate with the semantics an abstract interpreter so that reasoning about the semantics can be done by reasoning about computations on the interpreter. This technique is used to prove several facts about a semantics of pure LISP. First a denotatlonal semantics and an abstract interpreter are described. Then it is shown that the denotation of any LISP form is correctly computed by the interpreter. This is used to justify an inference rule - called "LlSP-induction" - which formalises induction on the size of computations on the interpreter. Finally LlSP-induction is used to prove a number of results. In particular it is shown that the function eval is correct relative to the semantics - i.e. that it denotes a mapping which maps forms (coded as S-expressions) on to their correct values.
Identifier:
CS-TR-1975-506
Contributor:
Gordon, Michael J. C. (autAuthor)
Type:
Text and technical reports
Date:
1975-08-01
Language:
engEnglish
Format:
1 text file, technical reports, and image/jpeg
Subject:
Stanford University. Computer Science Department and Computer science