Operational Reasoning and Denotational Semantics. AIM-264
Abstract/Contents
- Abstract
"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 semantic 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 denotational
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 "LISP-induction" which
formalises induction on the size of computations on the interpreter. Finally
LISP-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 asd S-expressions) on to
their correct values.
Description
Type of resource | text |
---|---|
Form | memorandums |
Extent | 1 text file |
Place | Stanford (Calif.) |
Date created | August 1975 |
Language | English |
Digital origin | reformatted digital |
Creators/Contributors
Author | Gordon, Michael |
---|
Subjects
Subject | Stanford Artificial Intelligence Laboratory |
---|---|
Subject | Memo (Stanford Artificial Intelligence Laboratory) |
Subject | Artificial intelligence |
Genre | Memorandums |
Bibliographic information
Finding Aid | |
---|---|
Memo | AIM-264 |
Location | https://purl.stanford.edu/mg771gp7582 |
Location | SC1041 |
Repository | Stanford University. Libraries. Department of Special Collections and University Archives |
Access conditions
- Use and reproduction
- The materials are open for research use and may be used freely for non-commercial purposes with an attribution. For commercial permission requests, please contact the Stanford University Archives (universityarchives@stanford.edu).
- Copyright
- Copyright © The Board of Trustees of the Leland Stanford Junior University. All rights reserved.
Collection
Stanford Artificial Intelligence Laboratory records, 1963-2009
View other items in this collection in SearchWorksAlso listed in
Loading usage metrics...