CMU-CS-01-129
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-01-129

Fixpoint Semantics for a Fragment of First-Order Linear Logic

Marco Bozzano*

May 2001

CMU-CS-01-129.ps
CMU-CS-01-129.pdf


Keywords: Linear logic, fixpoint semantics


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