This page collects work done by me and others on substructural logic programming. It focuses on forwardchaining substructural logic programming in which logic programming rules act roughly like rewriting rules  there are lot of interesting potential connections between forwardchaining substructural logic programming and rewriting logic semantics. This is distinct from backwardchaining or goaloriented logic programming in substructural logics.
A closely related project is the Security Protocol Specification Language MSR; Cervesato and Scedrov's 2009 journal paper "Relating StateBased and ProcessBased Concurrency through Linear Logic," mentioned in the list of papers below, describes the connection. Reasoning about substructural logic programs is one of the goals of the MetaCLF project (and one of the goals of my thesis!). Because the MetaCLF project page reviews work on this topic, I am only reviewing papers that discuss the specification or implementation of substructural logic programming languages.
Papers
Papers are listed in roughly chronological order.
 Monadic concurrent linear logic programming,
Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins, PPDP 2005.
This was an initial ambitious attempt to make a logic programming language combining both forwardchaining and backwardchaining based on Watkins et al.'s logical framework CLF. It introduced the Lollimon implementation; instructions for downloading and running Lollimon can be found at the bottom of this page. (Again, I didn't have anything to do with Lollimon, but there didn't seem to be instructions anywhere else on the web for how to download and run it!) The paper is available from the ACM Digital Library and Frank Pfenning's web page.
 Linear Logical Algorithms,
Robert J. Simmons and Frank Pfenning, ICALP 2008.
This paper gives a logical . Frank wrote up a short note, titled On Linear Inference, that discusses the philosophical basis for the style of forwardchaining we use in this paper.
The extended abstract published in ICALP 2008 is owned by Springer; the content in that extended abstract is also covered in the CMU tech report, which has the official CMU tech report number CMUCS08104 but didn't ever quite make it into the official CMU tech report archive, I believe.

Celf – A Logical Framework for Deductive and Concurrent Systems (System Description),
Anders SchackNielsen and Carsten Schürmann,
IJCAR 2008.
Describes Celf.
 Relating StateBased and ProcessBased Concurrency through Linear Logic, Iliano Cervesato and Andre Scedrov, IC 2009.

Substructural operational semantics as ordered logic programming,
Frank Pfenning and Robert J. Simmons,
LICS 2009.
Introduces Ollibot.
Presentation
This is the presentation of Linear Logical Algorithms from ICALP. I let myself fall slightly out of practice and was a bit under the weather when I recorded this; consider it an experiment, given that the presentation doesn't quite make sense without narration attached to the slides.
Lollimon
Lollimon is an experimental programming language that supports forward and backward chaining linear logical programming. It was originally described in the paper Monadic concurrent linear logic programming. The Linear Logical Algorithms paper describes a fragment of the Lollimon language, and so every LLA can be run in Lollimon. Note that Lollimon most definitely does not support the runtime guarantees described in the Linear Logical Algorithms paper.
The following commands will allow you to check out and build Lollimon. These instructions assume you have Ocaml installed on your system.
shell> cvs d :pserver:guest_lf@cvs.concert.cs.cmu.edu:/cvsroot login
(press Enter if prompted for a password  no password is necessary)
shell> cvs d :pserver:guest_lf@cvs.concert.cs.cmu.edu:/cvsroot checkout lollimon
shell> cd lollimon
shell> make
If everything goes correctly, you can then run the examples as follows. Starting Lollimon will cause you to enter Lollimon's toplevel environment.
shell> ./lollimon
LolliMon>#load "examples/linlogalg/spantree.lo"
[Loading file /Users/rjsimmon/Repos/lollimon/examples/linlogalg/spantree.lo]
Looking for 4 solutions to query: edge a b => edge a c => edge a d => edge b c => edge b e => edge d e => vertex a o vertex b o vertex c o vertex d o vertex e o {! (tree X Y)}
Attempt 1, Solution 1 with [X := d; Y := e]
Attempt 1, Solution 2 with [X := a; Y := b]
Attempt 1, Solution 3 with [X := a; Y := c]
Attempt 1, Solution 4 with [X := a; Y := d]
Success.
spantree.lo is Ok.
[Closing file /Users/rjsimmon/Repos/lollimon/examples/linlogalg/spantree.lo]
LolliMon>#quit
shell>
In this case, the four lines "Attempt 1, solution N" tell us that Lollimon's execution of the linear logical algorithm for spanning trees on the fiveelement undirected graph from the ICALP talk computed the spanning tree (a,b), (a,c), (a,d), (d,e).
In this manner, you can run all of the examples from the presentation and the ICALP paper, and most from the technical report. See the "README" file in the "lollimon/examples/linlogalg" directory.