Proofs and types. (English) Zbl 0671.68002

Cambridge Tracts in Theoretical Computer Science, 7. Cambridge etc.: Univ. Press. XI, 176 p. £17.50 (1989).
The book is based on the course of lectures on types \(\lambda\)-calculus given at the Université Paris VII in autumn 1986. It covers a wide spectrum of questions concerning proof theory, type theory and theoretical computer science. According to the principal epistemological idea that a good logic must possess a good operational semantics (the final aim is to extract programs from proofs) the main emphasis in the book is given to relating types terms to proofs and term conversions to proof normalizations. The book contains both introductory and advanced material, including natural deduction, sequent calculus, typed \(\lambda\)- calculus, Church-Rosser property, weak and strong normalization theorems for \(\lambda\)-calculus, the Curry-Howard isomorphism for (\(\wedge,\Rightarrow,\forall)\)-fragment of natural deduction, Gödel’s type system T (usual \(\lambda\)-calculus enriched with booleans, natural numbers, if-then-else, recursion operator and corresponding additional conversions).
One of the sections of the book is devoted to the proof of Hentzen’s cut elimination theorem (Hauptsatz) and its connection with resolution and the logic programming language PROLOG.
The advanced part of the book includes material on coherent spaces and stable functions, which give possibility to assign semantics to the system T and to the natural deduction system containing \(\vee\) and \(\exists\) and lead naturally to the linear logic. The type system F, an extension of simple typed \(\lambda\)-calculus, obtained by adding the abstraction operation on types is introduced. The abstraction on types is extremely powerful, giving possibility to define the usual data types such as integers and lists. It is proved that closed terms of type Int \(\to\) Int corresond precisely to recursive functions provably total in the second-order arithmetic \(PA_ 2\). The strong normalization theorem is proved for the system F.
One of the appendices to the book contains the description of semantics for the system F in terms of coherent spaces. The book is concluded with the appendix devoted to the linear logic (i.e. the logic without the weakening and contraction rules) which was originally discovered in coherence semantics and appears to be a promising approach in proof theory and computer science. The linear sequent calculus is introduced and proof nets providing a nice framework for cut elimination are discussed.
The book will be interesting for everybody working in proof theory and theoretical computer science.
Reviewer: G.Vorobyov


68-02 Research exposition (monographs, survey articles) pertaining to computer science
03B15 Higher-order logic; type theory (MSC2010)
03B40 Combinatory logic and lambda calculus
03F05 Cut-elimination and normal-form theorems
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03B70 Logic in computer science
03F07 Structure of proofs
03F10 Functionals in proof theory
03F35 Second- and higher-order arithmetic and fragments