loading...
Pi-Calculus in Logical Form
Wroclaw, Poland July 10-July 14
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2007.3622nd Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Marcello Bonsangue, Leiden University, the Netherlands
Alexander Kurz, University of Leicester, United Kingdom
Abramsky?s logical formulation of domain theory is extended to encompass the domain theoretic model for pi-calculus processes of Stark and of Fiore, Moggi and Sangiorgi. This is done by defining a logical counterpart of categorical constructions including dynamic name allocation and name exponentiation, and showing that they are dual to standard constructs in functor categories. We show that initial algebras of functors defined in terms of these constructs give rise to a logic that is sound, complete, and characterises bisimilarity. The approach is modular, and we apply it to derive a logical formulation of pi-calculus. The resulting logic is a modal calculus with primitives for input, free output and bound output.
Citation:
Marcello Bonsangue, Alexander Kurz, "Pi-Calculus in Logical Form," lics, pp.303-312, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.