In this paper we investigate the theoretical foundation of a bottom-up, fixpoint semantics for a subset of Girard's linear logic. More precisely, we consider a first-order formulation of a fragment of LinLog including multiplicative disjunction and universal quantification over goals. The semantics is defined by means of a fixpoint operator which is monotonic and continuous over an extended notion of interpretation lattice. We prove soundness and completeness of this semantics with respect to the usual operational semantics. We discuss some applications and related work.

22 pages

*DISI, Universita di Genova, Italy

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu