Paper: Equivalence of First Order LISP Programs. Proving Properties of Destructive Programs via Transformation (at LICS 1986)

Authors: Ian A. Mason

Abstract

In this paper we investigate various equivalence relations between expressions in first order LISP. This fragment of LISP includes the destructive operations rplaca and rplacd. To define the semantics we introduce the notion of a memory structure. The equivalence relations are then defined within this model theoretic framework. A distinction is made between intensional relations and extensional relations. The former class turn out to have a much more managable theory than the latter. The principle intensional relation studied is strong isomorphism, its properties allow for elegant verification proofs in a style similar to that of pure Lisp.

BibTeX

  @InProceedings{Mason-EquivalenceofFirstO,
    author = 	 {Ian A. Mason},
    title = 	 {Equivalence of First Order LISP Programs. Proving Properties of Destructive Programs via Transformation},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {105--117 },
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }