The expressive theory of stacks
The work
| Authors | Samuel Kamin |
|---|---|
| Editors | |
| Type | article |
| Year | 1987 |
| Citekey | kamin1987expressive |
Where it appeared
| Published in | Acta Informatica |
|---|---|
| Volume | 24 |
| Pages | 695--709 |
Identifiers
| DOI | 10.1007/bf00282622 |
|---|
Abstract
The usual theory of stacks is not expressive in the sense of C o o k ; that is, loop invariants needed to prove programs that use stacks cannot be stated in the logic. We first prove this assertion, then suggest ways of augmenting theories with new operators so as to achieve expressiveness. The main technique is to regard data types as function spaces. The technique is applied to stacks as well as to other data types.
A copy is held
pdf, 752.0 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-16 15:37 UTC |
Filed under
Cite it as
@article{kamin1987expressive,
title = {The expressive theory of stacks},
author = {Samuel Kamin},
year = {1987},
journal = {Acta Informatica},
volume = {24},
pages = {695--709},
doi = {10.1007/bf00282622},
}
This record lives at https://refs.drheap.org/kamin1987expressive/ and will keep doing so.