Computational aspects of linear logic
Patrick D. Lincoln · 1992
Linear logic was introduced by Girard in 1987 [30] both as a "logic behind logics", and as a "resource conscious logic". This thesis investigates computational aspects of linear logic. The main results of this work support the proposition that linear logic is a computational logic behind logics. This thesis augments the proof theoretic framework of linear logic by providing theorems such as permutability, impermutability, and cut-normalization with non-logical theories. On this expanded proof theoretic base, many complexity results are proved using a correspondence between proofs and computations. Among these results are the undecidability of propositional linear logic, the PSPACE-completeness of MALL, and the NP-completeness of the constant-only multiplicative fragment of linear logic. Another application of proof theory to computation is explored for a functional language ML-- and its (compiled) implementation. The proposed linear type system for ML-- yields compile-time type information about resource manipulation that may be useful in the control of some aspects of program execution such as storage allocation, garbage collection, and array update in place. Most general type and subject reduction theorems are proved, and a compiled implementation based on the Three Instruction Machine is described. Together, these results point out that linear logic is not about "Truth", it is about computation.