Linear logic and lazy computation

Abstract

Recently, J.Y. Girard discovered that usual logical connectors such as ⇒ (implication) could be broken up into more elementary linear connectors. This provided a new linear logic [Girard86] where hypothesis are (in some sense) used once and only once. The most surprising is that all the power of the usual logic can be recovered by means of recursive logical operators (connector “of course”). There are two versions of the linear logic: the intuitionistic one and the classical one. It seems that the second provides a appropriate formalism for parallelism and communication. This approach is entirely new and requires a further development. Here we restrict our attention to the intuitionistic version and to the consequences of the linear constraint to the computation process.