I've packaged that interpreter up into the following pieces of code.
The module lollisig.mod provides the basic signature for the Lolli language. Notice that to minimize the coding here, we are using the type o for both the type of lambda Prolog's formulas and Lolli's formulas. Usually, this double use of a type is a bad idea: with our modest ambitions here, it doesn't seem to cause any problems.
The module llinterp.mod is the actual Lolli interpreter rewritten into lambda Prolog syntax. The main interpretation feature it provides is the Input-Output modeel of resouces consumption, used to lazily divide resources when intepreting a tensor (multiplicative conjunction) or in backchaining.
This code can now be used as follows.
> elp Standard ML of New Jersey, Version 0.93, February 15, 1993 Elp, Version 0.1x, Built: Mon Mar 13 15:03:35 EST 1995 ?- load "lollisig", load "llinterp". [reading file ./lollisig.mod] .... [closed file ./lollisig.mod] [reading file ./llinterp.mod] .... [closed file ./llinterp.mod] solved yes ?- use "llinterp". ?- load "gaps". [reading file ./gaps.mod] .... [closed file ./gaps.mod] solved yes ?- use "gaps". ?- exrel N R, go (rel R nil). R = whom :: mary :: believes :: that :: bob :: married :: nil, N = 1. ; R = whom :: bob :: married :: nil, N = 2. ; no more solutions ?-Notice the way this last query was written: the query (exrel N R) is executed as a regular lambda Prolog query and (rel R nil) is executed as a Lolli query.
This version of the Lolli intepreter supports few non-logical features: only the is, read, write, and nl predicates are supported.
Logic Programming in a Fragment of Intuitionistic Linear Logic by Joshua S. Hodas and Dale Miller. Journal of Information and Computation, 110(2):327-365, 1 May 1994. (Postscript), (Abstract). Prolog code from this paper is available. An earlier version of this paper appeared in LICS'91.