A spatial logic for concurrency - II

Luís Caires, Luca Cardelli

Research output: Contribution to journalConference articlepeer-review

46 Citations (Scopus)
58 Downloads (Pure)


We present a modal logic for describing the spatial organization and the behavior of distributed systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to process composition and name hiding, and a fresh name quantifier. In Part I of this work we study the fundamental semantic properties of our logic; the focus of the present Part II is on proof theory. The main contributions are a sequent-based proof system for our logic, and a proof of cut-elimination for its first-order fragment.

Original languageEnglish
Pages (from-to)517-565
Number of pages49
JournalTheoretical Computer Science
Issue number3
Publication statusPublished - 6 Sep 2004
EventFoundations of Wide Area Network Computing - Malaga, Spain
Duration: 12 Jul 200213 Jul 2002


  • Distributed systems
  • Proof systems
  • Spatial logics
  • Specification
  • Verification


Dive into the research topics of 'A spatial logic for concurrency - II'. Together they form a unique fingerprint.

Cite this