Name
Abstract | ||
|---|---|---|
The authors present a formal system for deriving assertions about programs with side effects. The assertions considered are the following: (i) the expression e diverges (i.e. fails to reduce to a value); and (ii) e0 and e1 are strongly isomorphic (i.e. reduce to the same value and have the same effect on memory up to production of garbage). The e, ej are expressions of a first-order scheme- or Lisp-like language with the data operations atom, eq, car, cdr, cons, setcar, setcdr, the control primitives let and if, and recursive definition of function symbols |
Year | DOI | Venue |
|---|---|---|
1989 | 10.1109/LICS.1989.39183 | Pacific Grove, CA |
Keywords | Field | DocType |
equivalence classes,formal languages,recursive functions,Lisp-like language,control primitives,data operations,if,let,memory model,operational equivalence,operational semantics,programs with side effects,recursive definition of function symbols,semantic consequence,strongly isomorphic | Formal system,Discrete mathematics,Combinatorics,Formal language,Expression (mathematics),Recursive language,Isomorphism,Equivalence (measure theory),Equivalence class,Mathematics,Recursive definition | Conference |
Citations | PageRank | References |
23 | 6.27 | 4 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ian A. Mason | 1 | 797 | 97.47 |
| Carolyn Talcott | 2 | 1922 | 168.73 |