×

Notes on the simply typed lambda calculus. (English) Zbl 0933.03007

Berger, Ulrich (ed.) et al., Computational logic. Proceedings of the NATO ASI, Marktoberdorf, Germany, July 29–August 10, 1997. Berlin: Springer. NATO ASI Ser., Ser. F, Comput. Syst. Sci. 165, 57-97 (1999).
The simply typed lambda calculus, of these notes, has types built up from atomic types using the function type operation that forms a new type \(A\to B\) from types \(A\), \(B\). The calculus can be viewed as a refined version of the purely implicational fragment of intuitionistic logic. The refinement consists in using terms of the untyped lambda calculus to represent formal derivations of the logic.
These notes consist of three sections, the last one being on the simply typed lambda calculus. In that section I focus mainly on the Curry style version for function types, I call STT, that consists of rules for typing terms of the untyped lambda calculus. The middle section is on the untyped lambda calculus itself while the first section is mainly on the three standard styles of inference system for intuitionistic implicational logic; the Hilbert style, the natural deduction style and the sequent calculus style.
The main purpose of the notes is to act as a tutorial introduction to the three topics it treats and their relationships with each other. The novice reader is advised to read the notes in conjunction with the use of a more thorough text.
For the entire collection see [Zbl 0911.00047].

MSC:

03B40 Combinatory logic and lambda calculus
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03B20 Subsystems of classical logic (including intuitionistic logic)
03F03 Proof theory in general (including proof-theoretic semantics)
03F35 Second- and higher-order arithmetic and fragments
03F50 Metamathematics of constructive systems
PDFBibTeX XMLCite