Ludics Programming I: Interactive Proof Search
Alexis Saurin, Inria Futurs · 2007
Proof theory and Computation are research areas which have very strong relationships: new concepts in logic and proof theory often apply to the theory of programming languages. The use of proofs to model computation led to the modelling of two main programming paradigms which are functional programming and logic programming. While functional programming is based on proof normalization, logic programming is based on proof search. This approach has shown to be very successful by being able to capture many programming primitives logically. Nevertheless, important parts of real logic programming languages are still hardly understood from the logical point of view and it has been found very difficult t o give a logical semantics to control primitives. Girard introduced Ludics [12] as a new theory to study interaction. In Ludics, everything is built on interaction or in an i nteractive way. In this paper, which is the first of a series investigating a ne w computational model for logic programming based on Ludics, namely computation as interactive proof search, we introduce the interactive proof search procedure and study some of its properties.