A logic for strong late bisimilarity

We define logical counterparts for constructions 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