A General Adequacy Result for a Linear Functional Language

Abstract

A main concern of the paper will be a Curry-Howard interpretation of Intuitionistic Linear Logic. It will be extended with recursion, and the resulting functional programming language will be given operational as well as categorical semantics. The two semantics will be related by soundness and adequacy results. The main features of the categorical semantics are that convergence/divergence behaviour is modelled by a strong monad, and that recursion is modelled by ``linear fixpoints'' induced by CPO structure on the hom-sets. The ``linear fixpoints'' correspond to ordinary fixpoints in the category of free coalgebras w.r.t. the comonad used to interpret the ``of course'' modality. Concrete categories from (stable) domain theory satisfying the axioms of the categorical model are given, and thus adequacy follows in these instances from the general result.