##
**A primer on proofs and types.**
*(English)*
Zbl 0937.03063

Takahashi, Masako (ed.) et al., Theories of types and proofs. Based on the workshop, Tokyo, Japan, September 1997. Tokyo: Mathematical Society of Japan. MSJ Mem. 2, 1-44 (1998).

The article under review is expository and yields an introduction to the area of proof systems and type systems.

After a brief historical opening, the proper mathematical part begins with section 2, where we find (i) the natural deduction system NK and the Gödel completeness theorem; (ii) the intuitionistic system NJ, as justified by the BHK-semantics, with a hint toward sequent calculi. The third section is a sort of compact introduction to computability (both via recursive schemata and a simplifed programming language based on assignement/while statements).

Section 4, devoted to the type-free lambda calculus, bridges the gap between proof systems and type systems. Technically, the author surveys the basic properties of lambda calculus (Church-Rosser theorem, standardization, lambda definability of recursive functions).

Section 5 offers an exposition of the basic simply typed lambda calculus, with a proof of the strong normalization theorem (in outline), and an excursion towards Gödel’s system T of primitive recursive functionals of finite type. Next, the author defines Girard’s system \(\lambda 2\) of second-order lambda calculus and sketches an extension of strong normalization for \(\lambda 2\). The survey also embraces higher-order systems, up to including the calculus of constructions.

As to be expected, the real backbone of the paper is the connection between type systems and proof systems, which exploits the fundamental Curry-Howard isomorphism between formulas and types (proofs and functionals, respectively).

We find the paper a well-structured and readable addition to the existing literature in the area.

For the entire collection see [Zbl 0919.00041].

After a brief historical opening, the proper mathematical part begins with section 2, where we find (i) the natural deduction system NK and the Gödel completeness theorem; (ii) the intuitionistic system NJ, as justified by the BHK-semantics, with a hint toward sequent calculi. The third section is a sort of compact introduction to computability (both via recursive schemata and a simplifed programming language based on assignement/while statements).

Section 4, devoted to the type-free lambda calculus, bridges the gap between proof systems and type systems. Technically, the author surveys the basic properties of lambda calculus (Church-Rosser theorem, standardization, lambda definability of recursive functions).

Section 5 offers an exposition of the basic simply typed lambda calculus, with a proof of the strong normalization theorem (in outline), and an excursion towards Gödel’s system T of primitive recursive functionals of finite type. Next, the author defines Girard’s system \(\lambda 2\) of second-order lambda calculus and sketches an extension of strong normalization for \(\lambda 2\). The survey also embraces higher-order systems, up to including the calculus of constructions.

As to be expected, the real backbone of the paper is the connection between type systems and proof systems, which exploits the fundamental Curry-Howard isomorphism between formulas and types (proofs and functionals, respectively).

We find the paper a well-structured and readable addition to the existing literature in the area.

For the entire collection see [Zbl 0919.00041].

Reviewer: Andrea Cantini (Firenze)

### MSC:

03F03 | Proof theory in general (including proof-theoretic semantics) |

03B40 | Combinatory logic and lambda calculus |

03-01 | Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations |

03F07 | Structure of proofs |

03F10 | Functionals in proof theory |