Ian A. Mason
The computer-programming language LISP is well understood in theory but in practice is subject to "destructive operation" that manipulate data and cause problems in program specification, derivation, verification, and transformation. Using a notion of memory structure that adequately models destructive operations, Mason develops a theory that accounts for actual practice, and he offers suggestions for improving practice within this theory. He then investigates and defines important equivalence relations in LISP programs.
Ian A. Mason is a researcher at the Laboratory for Foundations of Computer Science at Edinburgh University.
- Chapter 1 Introduction
- 1.1 A Little History
- 1.2 The Underlying Data Structure
- 1.3 An Outline
- 1.4 Notation
- Chapter 2 The Basic Theory of Memory Structure
- 2.1 Memory Structure
- 2.2 Computing over Memory Structures
- Chapter 3 Equivalence Reltations
- 3.1 Isomorphic and Lisp Equality
- 3.2 Strong Isomorphism
- 3.3 The Substitution Theorem
- 3.4 Axioms for ≃
- 3.5 An Example of a Proof
- 4 A Plethora of Simple Examples
- 4.1 Example 0: The inplace:reverse Program
- 4.2 Example 1: The Recursive copy Program
- 4.3 Example 2: Substitution Programs
- 4.4 Example 3: A Sophisticated Length Program
- 4.5 Example 4: The iterative:append Program
- 4.6 Example 5: The nconc Program
- 4.7 Example 6: The List Reversing Programs Revisited
- 4.8 Example 7: List Copying Programs
- 4.9 Example 8: Queue Representation and Manipulation
- 4.10 Example 9: The Substitution Programs Revisited
- 4.11 Example 10: The Deutsch-Schorr-Waite Marking Algorithm
- 4.12 Example 11: The Morris Traversal Algorithm
- Chapter 5 The Effectiveness Theorems
- 5.1 The Underlying Logic
- 5.2 Partial Memories and Memory Schemata
- 5.3 The Symbolic Evaluation Relation >𝕊
- 5.4 The Proofs of Theorems A and B
- 5.5 The Proof of Theorem C
- 5.6 The Proof of Theorem D
- 5.7 Previous Results
- Chapter 6 Fragments of Lisp
- 6.1 Equivalence Relations Revisited
- 6.2 The Structure of 𝕄pure Definable Functures
- 6.3 The Interrelationships
- Chapter 7 Derivations and Transformations
- 7.1 The Rules of Scherlis
- 7.2 THe Transformation Rules
- Chapter 8 The Robson Marking Algorithm and Applications
- 8.1 The Robson Marking Program
- 8.2 An APplication of the Robson Marking Algorithm
- 8.3 A Description of the Transformation T
- 8.4 The Robson Copying Algorithm
- 8.5 The Proof of the Marking Theorem
- 8.6 The Proof of the Peeling Theorem
- Chapter 9 Programs as Data and the Eval function
- 9.1 The Syntax of the Internal Programming Language
- 9.2 The Semantics of the Internal Programming Language
- 9.3 The Definition of eval
- 9.4 The Real-Eval-Print Loop
- 9.5 Correctness in the eval Program
- Chapter 10 Editing Data Efficiently
- 10.1 Commands
- 10.2 The Code for the Editor
- 10.3 A Sample Editing Session
- 10.4 Proving Properties of the Editor
- Chapter 11 Conclusions
- 11.1 Summary
- 11.2 Richer Languages
- 11.3 Foundations for the Analogy
- Bibliography
1/1/1986
