Martin Churchill, A Logic of Sequentiality
Martin Churchill (University of Bath, UK)
A Logic of Sequentiality
It is well established through the Curry-Howard isomorphism that functional programs have a correspondence with proofs in intuitionistic logics; we say the corresponding functional program is the computational content of the proof. But what kind of proofs exist whose computational content is an imperative, perhaps object-orientated, program? To answer this question, it is natural to look at denotational models of such languages, of which the primary examples are games models.
Here we present a new affine logic WS where proofs represent history-sensitive winning strategies, and hence imperative programs. We can embed (for example) Polarised Linear Logic inside WS, but we also obtain new proofs that correspond to imperative programs. Using categorical properties of the model we obtain a full completeness result: a semantics-guided proof search procedure ensuring each history-sensitive strategy is the semantics of a unique cut-free core proof. We can use this result to derive an explicit cut elimination procedure.