A logic for strong late bisimilarity (Part II)

We define logical counterparts forconstructions including dynamic name allocation and name exponentiation and show that they are dual to standard constructs in functor categories. In particular, we show that the final coalgebra of a functor defined by Stark and Fiore, Moggi and Sangiorgi in terms of these constructs give rise to a logic for the pi-calculus that is sound, complete, expressive and respects strong late bisimilarity. The resulting logic is a modal calculus with primitives for input, free output and bound output.  

hosted by