Abstract

Logic programming can be given a foundation in sequent calculus by viewing computation as the process of building a cut-free sequent proof bottom-up. The first accounts of logic programming as proof search were given in classical and intuitionistic logic. Given that linear logic allows richer sequents and richer dynamics in the rewriting of sequents during proof search, it was inevitable that linear logic would be used to design new and more expressive logic programming languages. We overview how linear logic has been used to design such new languages and describe briefly some applications and implementation issues for them.

Introduction

It is now commonplace to recognize the important role of logic in the foundations of computer science. When a major new advance is made in our understanding of logic, we can thus expect to see that advance ripple into many areas of computer science. Such rippling has been observed during the years since the introduction of linear logic by Girard in 1987. Since linear logic embraces computational themes directly in its design, it often allows direct and declarative approaches to computational and resource sensitive specifications. Linear logic also provides new insights into the many computational systems based on classical and intuitionistic logics since it refines and extends these logics.

There are two broad approaches by which logic, via the theory of proofs, is used to describe computation. One approach is the proof reduction paradigm, which can be seen as a foundation for functional programming. Here, programs are viewed as natural deduction or sequent calculus proofs and computation is modeled using proof normalization.