[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Reasoning about queues



Hi,
I would like to know if someone has a good theory of queues. 
I would like one that is built in such a way that allows good use of
rewriting (i.e. doesn't get (grind) into infinite rewriting loops).

(I need FIFO unbounded queues for objects of any nonempty type).

I am trying with a definitional style based on finite_sequence,
but I was thinking an axiomatic style might lead to more efficient proofs.

Thanks,

Marcelo Glusman