1987年にJ.-Y. Girardが発表した線形論理は，計算機科学への応用が期待さ れている新しい論理体系である．線形論理の論理型言語への応用は，特に活 発な分野の一つであり，LO, ACL, Lolli, Lygon, Forum, およびLLP等の研 究がある．これらのほとんどの言語では，リソース概念はプログラミング上 で重要な位置を占めている．したがって，リソースを効率的良く取り扱う計 算モデルの構築は重要な研究課題となっている．本論文で述べるレベル付き IOモデルは，効率的なリソース管理を目的とした計算モデルであり，実行中 はただ一つのリソース表を保持すれば良いように工夫されている．本モデル は，LLPコンパイラ処理系で採用され，その有効性が示されている．

LLPの計算モデルであるレベル付きIOモデルについてまとめた論文．

本論文では，線形論理に基づいた論理型言語LLPの概要と，そのコンパイラ 処理系のための抽象機械であるLLPAMについて述べている．LLPは，Prologの 自然な拡張になっており，論理式をリソースとして取り扱うことができる点 を特徴とする．抽象機械LLPAMは，LLPの効率的な計算モデルであるレベル付 きIOモデルのリソース管理方式に基づいて設計されており，抽象機械WAMの 拡張になっている．LLPAMでは，リソース自体もコンパイルされており，ま たリソースの検索はハッシュ表を通じて行われるため，線形論理型言語の特 徴であるリソース論理式の追加や消費といった操作を非常に効率よく実現す ることができる．

LLPのコンパイラ処理系で用いているLLPAM (LLP抽象機械)についてまとめた論文．

A number of logic programming languages based on Girard's Linear Logic have been proposed. While efficiency of computation has been a consideration in the design of these languages from the earliest days the proposed implementation techniques have relied heavily on the copying and scanning of large data structures to ensure that linearity conditions have been met, and thus have been most suited to the creation of interpreters written in high-level languages. In this paper we present a new formulation of the logic of the the language Lolli that is conducive to the creation of both more efficient interpreters, as well as compilers based on extensions of the standard WAM model. We present an extension of the WAM based on this model which implements a useful fragment of Lolli. Resource conscious algorithms executed using this system show significant performance advantages relative to their traditional Prolog implementations.

LLPの計算モデルと抽象機械について述べた論文．リソース式のコンパイルについては述べられていない．

There have been several proposals for logic programming language based on linear logic: Lolli, Lygon, LO, LinLog, Forum.
In addition, BinProlog allows the use of linear implications of affine logic (a variant of linear logic). In these languages, it is possible to create and consume resources dynamically as logical formulas. The efficient handling of resource formulas is therefore an important issue in the implementation of these languages.
In [10], N. Tamura and Y. Kaneda proposed an abstract machine called LLPAM which is an extension of the standard WAM for a linear logic programming language called LLP. LLP is a superset of Prolog and a subset of Lolli. However, in the original LLPAM design, a resource formula was stored as a term in a heap memory and was not compiled into LLPAM code.
In this paper, we describe an extension of LLPAM for compiling resource formulas. In our extension, resources are compiled into closures which consist of compiled code and a variable binding environment.

LLPのリソース式のコンパイルについて述べた論文．

LLPの言語と処理系について述べた初期の論文．

LLPの言語と処理系の概要について述べた初期の論文．

時相線形論理に基づいたTLLPの言語について述べた論文．

時相線形論理に基づいたTLLPのコンパイラ処理系について述べた論文．

時相線形論理に基づいたTLLPのコンパイラ処理系について述べた論文．

When Prolog programs that manipulate lists to manage a collection of resources are rewritten to take advantage of the linear logic resource management provided by the logic programming language Lolli, they can obtain dramatic speedup. Thus far this has been demonstrated only for ``toy'' applications, such as n-queens. In this paper we present such a reimplementation of the lean connection-calculus prover lolliCoP and obtain a theorem prover for first-order classical logic which rivals or outperforms state-of-the-art provers on a significant body of problems.

一階述語論理の節形式をPrologプログラムに変換し， Prologコンパイラ処理系を用いて定理証明を 行うシステムとしてPTTP (Prolog Technology Theorem Prover)が 知られている． 本論文では，節形式を線形論理型言語LLPのプログラムに変換し， LLPコンパイラ処理系を用いることで， より効率的な証明探索が可能になることを示す． 特に，証明中のリテラルをリソースとして追加することにより， ME (model elimination)処理を高速化している点に特徴がある．

本論文では， 著者らの開発した線形論理型言語コンパイラ処理系のLLPを用いて， 古典命題線形論理の論理式の証明探索を行うシステムLL2LLPについて述べる． 本システムは，古典命題 線形論理式を直観主義線形論理式に変換し，さらにLLPコンパイラを用いてLLP 抽象機械命令にコンパイルしたのち実行することで高速な証明探索を実現して いる点に特徴がある． いくつかの線形論理式に対して，既存の線形論理定理証明システムと 性能を比較した所， ほとんどの問題でより良い結果が得られた．