Towards a linear contract logic

Post date: 11-Sep-2013 13:10:55

Upcoming Seminar

Towards a linear contract logic

ICTCS 2013

September 9-11, 2013

Università degli Studi di Palermo

Paolo Di Giamberardino

Dipartimento di Matematica e Informatica - Università degli Studi di Cagliari

Abstract. 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.

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.