Towards a linear contract logic (Extended Abstract)


Paolo Di Giamberardino, Massimo Bartoletti, Roberto Zunino

14th Italian Conference on Theoretical Computer Science


We introduce a linear logic for contracts. The logic (called PCLLW) extends intuitionistic linear affine logic ILLW with a contractual implication connective, along the lines of Propositional Contract Logic (PCL). A proof system for PCLLW is presented, and it is shown sound and complete with respect to a phase structure model. By exploiting the finite model property, we show that PCLLW is decidable.

Download: pcll-ictcs.pdf