Lambda calculus and Type Theory

The lambda calculus was originally conceived by Church in 1932 as part of a general theory of functions and logic, intended as a foundation for mathematics. Although the system turned out to be inconsistent, the subsystem dealing with functions only became a succesful model for the computable functions. This system is called now the (type-free) lambda calculus. Representing computable functions as lambda terms gives rise to so called functional programming.

In the lambda calculus above every expression, considered as a function, may be applied to every other expression, considered as an argument. In the typed versions of the lambda calculus types are assigned to terms. Now a term M may be applied to a term N of type A only if M has type A-->B for some type B. A term may be considered as a program and a type of that term as a specification of that program. But that is not the only possibility. A type can also be viewed as a proposition and a term of this type as a proof of this proposition. Several systems of proof checking are based on this interpretation of propositions-as-types and proofs-as-terms.

People::

• Henk Barendregt

• Wil Dekkers

• Herman Geuvers

• Jan Willem Klop

• Iris Loeb

Projects::

• Typed Lambda Calculus and Applications.

  • The aim is to produce a research monograph on typed lambda calculus with its mentioned applications. This book will serve as a sequel to Barendregt's monograph on type-free lambda calculus (North-Holland, 1984, also translated into Russian and Chinese), a classical work that is considered as the standard reference to lambda calculus. The editors and main authors of the book are Henk Barendregt and Wil Dekkers of the University of Nijmegen and Rick Statman of Carnegie Mellon University, Pittsburgh, USA. Several co-authors (all of them leading experts in the field) will contribute to this work. The project is embedded in the larger project `Lambda-calculus and Applications', a 7-year research effort at the Computing Science Institute in Nijmegen, supported by a special grant of the University Council.

• Illative Combinatory Logic.

  • In this project we study relations between ordinary logic and illative combinatory logic. We fulfilled the program of Curry and Church to find sound and complete interpretations of intuitionistic propositional and predicate logic into systems of illative combinatory logic. Joint work of Henk Barendregt and Wil Dekkers with Martin Bunder, University of Wollongong, Australia.

• Study of the Simple Types.

  • In this project Thierry Joly studies slantwise lambda-definable functions,characterisations of the finitely generated types, and the 'Proof as Program' paradigm.