Sequent Calculus and the Specification of Computation

The sequent calculus has been used for many purposes in recent years within theoretical computer science. In these lectures, we shall highlight some of its uses in the specification of and reasoning about computation.During the search for cut-free sequent proofs, the formulas in sequents are re-arranged and replaced with other formulas. Such changes can be used to model the dynamics of computation in a wide range of applications. For various reasons, we shall be interested in “goal-directed proof search” and will examine intuitionistic logic and linear logic for subsets that support this particularly simple form of search. We will show, quite surprisingly, that with the appropriate selection of logical connectives, goal-directed search is complete for all of linear logic. This fact leads naturally to the design of a logic programming-like language based on linear logic. The resulting specification language, called Forum, is an expressive and rich specification language suitable for a wide range of computational paradigms.After providing an overview of sequent calculus principles, we shall develop the notion of goal directed search for a variety of logics, starting with the intuitionistic logic theory of Horn clauses and hereditary Harrop formulas. We shall provide various example specifications in these logics, especially examples that illustrate how rich forms of abstractions can be captured. Finally, we briefly indicate how the notion of goal-directed proof search can be extended to linear logic.No advanced knowledge of the sequent calculus or of linear logic will be assumed, although some familiarity with their elementary syntactic properties will be useful. Similarly, some acquaintance with the basic concepts of the lambda-calculus and intuitionistic logic will also be useful.