Preface

The Curry-Howard isomorphism, also widely known as the “propositions-as-types” paradigm, states an amazing correspondence between systems of formal logic and computational calculi.1 It begins with the observation that an implication A → B corresponds to a type of functions from A to B, because inferring B from A → B and A can be seen as applying the first assumption to the second one—just like a function from A to B applied to an element of A yields an element of B. Similarly, one can argue that proving the implication A → B by actually inferring B from A resembles constructing a function that maps any element of a domain A into an element of B.

In fact, it is an old idea—due to Brouwer, Kolmogorov, and Heyting—that a constructive proof of an implication from A to B is a procedure that transforms proofs of A into proofs of B. The Curry-Howard isomorphism formalizes this idea so that, for instance, proofs in the propositional intuitionistic logic are represented by simply typed λ-terms. Provable theorems are nothing else than non-empty types.

This analogy, first discovered by Haskell Brooks Curry in the 1930’s, has turned out to hold for other logical systems as well. Virtually all proof-related concepts can be interpreted in terms of computations, and virtually all syntactic features of various lambda-calculi and similar systems can be formulated in the language of proof theory. For instance, quantification in predicate logic corresponds to dependent product, second-order logic is connected to polymorphism, and proofs by contradiction in classical logic are close relatives of control operators, e.g. exceptions. Moreover, various logical formalisms (Hilbert style, natural deduction, sequent calculi) are mimicked by corresponding models of computation (combinatory logic, λ-calculus, and explicit substitution calculi).

Since the 1969 work of William Howard it has been understood that the proposition-as-types correspondence is not merely a curiosity, but a fundamental principle. Proof normalization and cut-elimination are another model of computation, equivalent to β-reduction. Proof theory and the theory of computation turn out to be two sides of the same field.

Recent years show that this field covers not only theory, but also the practice of proofs and computation. Advanced type theory is now used as a tool in the development of software systems supporting program verification and computer-assisted reasoning. The growing need for efficient formal methods presents new challenges for the foundational research in computer science.

For these reasons the propositions-as-types paradigm experiences an increasing interest both from logicians and computer scientists, and it is gradually becoming a part of the curriculum knowledge in both areas. Despite this, no satistfactorily comprehensive book introduction to the subject has been available yet. This volume is an attempt to fill this gap, at least in the most basic areas.

Our aim is to give an exposition of the logical aspects of (typed) calculi (programs viewed as proofs) and the computational aspects of logical systems (proofs viewed as programs). We treat in a single book many issues that are spread over the literature, introducing the reader to several different systems of typed λ-calculi, and to the corresponding logics. We are not trying to cover the actual software systems (e.g. Coq) based on the formulas-as-types paradigm; we are concerned with the underlying mathematical principles.

Although a great deal of our attention is paid to constructive logics, we would like to stress that we are entirely happy with non-constructive meta-proofs and we do not restrict our results to those acceptable to constructive mathematics.

An idea due to Paul Lorenzen, closely related to the Curry-Howard isomorphism, is that provability can be expressed as a dialogue game. Via the Curry-Howard isomorphism, terms can be seen as strategies for playing such games. While for us proofs and programs are more or less the same objects, we would hesitate to claim the same thing about dialogue games or strategies for such games. Nevertheless, there is an emerging picture that the Curry-Howard isomorphism is perhaps about three worlds, not two, or that all three worlds are one. We also go some way to convey this paradigm.

An important subject, the linear logic of J.-Y. Girard, is not treated here, although it is very close to the subject. In fact, linear logic (and related areas—geometry of interaction, ludics) opens an entire new world of connections between proofs and computations, adding new breathtaking perspectives to the Curry-Howard isomorphism. It deserves a broader and deeper presentation that would have to extend the book beyond reasonable size. After some hesitation, we decided with regret not to treat it at all, rather than to remain with a brief and highly incomplete overview.

As we have said above, our principal aim is to explore the relationship between logics and typed lambda-calculi. But in addition to studying aspects of these systems relevant for the Curry-Howard isomorphism, we also attempt to consider them from other angles when these provide interesting insight or useful background. For instance, we begin with a chapter on the type-free λ-calculus to provide the necessary context for typed calculi.

The book is intended as an advanced textbook, perhaps close to the border between a textbook and a monograph, but still on the side of a textbook. Thus we do not attempt to describe all current relevant research, or provide a complete bibliography. Sometimes we choose to cite newer or more comprehensible references rather than original works. We do not include all proofs, though most are provided. In general we attempt to provide proofs which are short, elegant, and contain interesting ideas. Though most proofs are based on solutions known from the literature, we try, whenever possible, to add a new twist to provide something interesting for the reader. Some new results are included too.

The book may serve as a textbook for a course on either typed λ-calculus or intuitionistic logic. Preferably on both subjects taught together. We think that a good way to explain typed λ-calculus is via logic and a good way to explain logic is via λ-calculus.

The expected audience consists mainly of graduate and PhD students, but also of researchers in the areas of computer science and mathematical logic. Parts of the text can also be of interest for scientists working in philosophy or linguistics.

We expect that the background of the readers of this book may be quite non-uniform: a typical reader will either know about intuitionistic logic or about λ-calculus (and functional programming), but will not necessarily be familiar with both. We also anticipate readers who are not familiar with any of the two subjects.

Therefore we provide an introduction to both subjects starting at a relatively elementary level. We assume basic knowledge about discrete mathematics, computability, set theory and classical logic within the bounds of standard university curricula. Appendix A provides some preliminaries that summarize this knowledge. Thus the book is largely self-contained, although a greater appreciation of some parts can probably be obtained by readers familiar with mathematical logic, recursion theory and complexity.

We hope that the bibliographical information is reasonably up to date. Each chapter ends with a Notes section that provides historical information and also suggests further reading. We try to include appropriate references, but sometimes we may simply not know the origin of a “folklore” idea, and we are sorry for any inaccuracies.

Each chapter is provided with a number of exercises. We recommend that the reader try as many of these as possible. Hints or solutions are given for some of the more difficult ones, hopefully making the book well-suited for self-study too. Some exercises are used as an excuse for including something interesting which is not in the mainstream of the book. The reader is also expected by default to do all omitted parts of proofs by herself.

Earlier versions of this text (beginning with the DIKU lecture notes [450]) have been used for several one-semester graduate/Ph.D. courses at the Department of Computer Science at the University of Copenhagen (DIKU), and at the Faculty of Mathematics, Informatics and Mechanics of Warsaw University. Summer school courses have also been held based on it.

Acknowledgments

Just like many other milestone ideas, the Curry-Howard isomorphism was discovered to various extents by different people at different times. And many others contributed to its development and understanding. The Brouwer – Heyting – Kolmogorov – Schönfinkel – Curry – Meredith – Kleene – Feys – Gödel – Läuchli – Kreisel – Tait – Lawvere – Howard – de Bruijn – Scott – Martin-Löf – Girard – Reynolds – Stenlund – Constable – Coquand – Huet –…–...