Notes on the simply typed lambda calculus
Church-Rosser theoremcombinatory logicHilbert style inference systemnatural deductionnormalizationrefined version of the purely implicational fragment of intuitionistic logicsequent calculussimply typed lambda calculussimply typed theory STTtutorial introductionuntyped lambda calculus
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Proof theory in general (including proof-theoretic semantics) (03F03) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)
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].
- Some lambda calculus and type theory formalized
- A finite axiomatization of propositional type theory in pure lambda calculus
- scientific article; zbMATH DE number 431764 (Why is no real title available?)
- scientific article; zbMATH DE number 177773 (Why is no real title available?)
- The use of the typed lambda calculus for guiding naive users in the representation and acquisition of part-whole knowledge
- Pruning simply typed -terms
- Introduction to Type Theory
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
This page was built for publication: Notes on the simply typed lambda calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4263831)
