Towards a linear contract logic
Massimo Bartoletti, Paolo Di Giamberardino, Roberto Zunino · UNICA IRIS Institutional Research Information System (University of Cagliari) · 2013
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.