- Computational interpretations of linear logic by Samson Abramsky provides the notion of proof terms for linear logic that can be interpreted as an executable program. [Theor. Comput. Sci. 111(1&2): 3-57 (1993)]
- Operational Interpretations of Linear Logic by Turner and Wadler describes another operational interpretation for linear logic. [Theoretical Computer Science, to appear. (2006?)]. I belive that this is the latest development along the lines that Nick Benton describes in A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models in Proceedings of Computer Science Logic 1994, Kazimierz, Poland. Springer-Verlag LNCS 933. June 1995. These approaches are all much like: Dual Intuitionistic Linear Logic (1996) by Barber and Plotkin. An account of intuitionistic linear logic designed to reflect the motivation of exponentials as translations of intuitionistic types, and provide it with a term calculus, proving associated standard type-theoretic results. I believe Plotkin initially proposed this approach, which splits the context into two kinds.
- A syntax for linear logic Philip Wadler, Ninth International Conference on the Mathematical Foundations of Programming Semantics, Springer Verlag LNCS 802, New Orleans, Lousiana, April 1993. and There's no substitute for linear logic Philip Wadler. 8'th International Workshop on the Mathematical Foundations of Programming Semantics, Oxford, April 1992. These give another semantics for linear logic, separating each kind of assumption in the context intwo two kinds: linear and intuitionistic.

- Sara Kalvala and Valeria de Paiva have formalised propositional linear logic in Isabelle. Although they are no longer working on this, they have written a paper describing this work, which is available here. Sara Kalvala has also written a paper with Mike Squire that describe how HOL can be embedded within their formalisation, available here.
- Philippe de Groote, in the CALLIGRAMME project, has written a paper titled Linear Logic with Isabelle: Pruning the Proof Search Tree, in TABLEAUX 1995: 263-277. This describes the development of tactics in Isabelle to automate proof search in Linear Logic.
- Mechanized separation logic (slightly related to linear logic) in Isabelle by Tjark Weber
- James Power and Caroline Webster have formalised linear logic in coq (TPHOLs99) Working with Linear Logic in Coq. James Power et al. have also looked at protocols in several logics, including intuitionistic linear logic, in Four Logics and a Protocol (1999) and have also made further studies of protolocs with linear logic in A Specification of TCP/IP using Mixed Intuitionistic Linear Logic (Extended Abstract) (2001) and Specifying and Verifying Communications Protocols using Mixed Intuitionistic Linear Logic (2005).

- Resource-conscious AI planning with conjunctions and disjunctions - Peep Küngas: a resource-conscious Artificial Intelligence (AI) planning system, which allows for nondeterminism in the environment. The system is called RAPS. Last update in 2002.
- Ozan Kahramanogullari is using an extension of linear logic, which has evolved into the Calculus of Structures, and also developing proof search techniques for his system. In his own words, he is "... developing a common language for concurrency and planning that aims at bringing these two fields closer. Such a language will allow to transfer mathematical notions from concurrency to planning, and provide a platform for a structural analysis of plans.". This work is in the Maude system. Papers are available at http://alessio.guglielmi.name/res/cos/index.html.
- Stephen Cresswell's PhD thesis describes a Prolog implementation of Linear Logic which was used to synthesise plans. This work was published with Smaill and Richardson in the 5th European Conference on Planning (ECP 99). It can be found at here.
- G. Gallegos Ayala MSc thesis Plans from Proofs reimplements some of Stephen Cresswell's PhD work within Lambda Prolog.
- The PhD thesis of Jinghai Rao, Semantic Web Service Composition via Logic-based Program Synthesis, describes using linear logic for the composition of web services. This work uses a loose coupling of systems which are combined using an agent framework and translations between the various languages. For linear logic proof construction, they use LL-prover. They argue that linear logic based composition of web services is feasible, and that they have provided a flexible and scalable agent based system. However, they do not describe any large case studies. It may be that case studies are described in the associated papers.
- The PhD thesis of Sven Lammermannm, "Runtime Service Composition via Logic-Based Program Synthesis", describes a declarative object orientated programming language and a synthesis technique which is used to compose services. They provide a prototype system and partial automation.
- Paulo Pinheiro da Silva, Deborah L. McGuinness and Richard Fikes. A Proof Markup Language for Semantic Web Services. Information Systems. [Accepted for publication.] and Paulo Pinheiro da Silva, Patrick Hayes, Deborah L. McGuinness, Richard Fikes and Priyendra Deshwal. Towards Checking Hybrid Proofs. Technical Report KSL-05-01, Knowledge Systems Labora tory, Stanford University, USA, 2005. see: http://iw.stanford.edu/documents_papers.html

- In Giorgi Japaridze's PhD thesis, The logic of resources and tasks, University of Pennsylvania, Philadelphia, 1998, 145 pages, a semantics where statements are tasks is given for the decidable multiplicative-additive (exponential-free) fragment of Linear Logic. He argues that this an appropriate formalism for planning.

- Lolli: A linear Logic Programming Language. (last update '95)
- LLF: The Linear Logical Framework. (last update '98). I think the implementation is at: Linear Twelf, and the paper is "A linear logical framework".
- LLP: A Linear Logic Programming Language and its Compiler System - LLP is a logic programming language based on intuitionistic linear logic. LLP is a superset of Prolog and a subset of Lolli developed by Josh Hodas and Dale Miller. (last update '03)
- The PrologCafe project provides a Prolog to Java translator which supports translation of the LLP language (based on Intuitionistic Linear Logic and used by the Lolli system) into Java. This provides a way of compiling and executing (the LLP subset) Lolli programs in Java. (last update '04)
- LLProver: a theorem prover for linear logic. (last update to prover '97, last update to website Jan '05 - but note that most of the links are broken or irrelavent.)
- Tanel Tammet has written a tableux prover for linear logic. (Aprox '94). Related to the paper "Proof Sytrategies in Linear Logic." J. Autom. Reasoning 12(3): 273-304 (1994)
- MALL A small prolog implementation of linear logic. I think think this is originally by Natarajan Shankar.
- YahOO:Yet another higher-order Object-Oriented Language. This is an object oriented programming language, written in LambdaProlog, based on Linear Logic. (last update '95). This work has become the PRObjLOG = PROLOG + OBJECTS project, which is implemented in Lolli.

- Detecting Loops During Proof Search in Propositional Affine Logic by Tatjana Lutovac and James Harland

- Deductive synthesis of astronomical software using the Maude term rewriting system Anthony Castanares, University of Texas at El Paso (PhD Dissertation, 2003)

- The 2000 LINEAR international Summer School (Linear Logic and Applications).
- The LINEAR project - focused on developing the theory and the applications of Linear Logic.
- The Forum Specification Language - a presentation of all of higher-order linear logic that makes it into a logic programming language.