-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2018.STLC.Kripke
Fabian edited this page Nov 3, 2021
·
4 revisions
by Frederik Folkmar Ramcke
This week I will present two ways of giving semantics to the simply typed lambda calculus (STLC): Henkin semantics and Kripke semantics. While the former correspond more naturally to how we intuitively assign meaning to STLC terms, they are not complete (for some notion of completeness). Hence the main focus of the talk, which will be a presentation of Kripke-style semantics (based on [1]) for which we will derive a well-known completeness theorem.
If time permits I would also like to discuss one or multiple of the following related points:
- the different notions of completeness and their relation to the presentation of STLC as a computational calculus vs. an intuitionistic propositional logic
- how 'normalisation by evaluation' arises from the completeness proof
- how we can frame both Henkin and Kripke semantics as special cases of categorical semantics in cartesian closed categories
- [^] John C. Mitchell, Eugenio Moggi. Kripke-Style Models for Typed lambda Calculus. Ann. Pure Appl. Log. 51(1-2), pp. 99-124, 1991.
- Leon Henkin. Completeness in the Theory of Types. Journal of Symbolic Logic 15(2), pp. 81-91, 1950.
- Harvey Friedman. Equality between functionals. Logic Colloquium 1972, pp. 22-37. Lecture Notes in Mathematics 453, Springer 1975.
- Albert R. Meyer. What is a Model of the Lambda Calculus? Information and Control 52(1), pp. 87-122, 1982. Note: For the claim that environment/natural semantic models and combinatory models are equivalent notions see the "Combinatory Model Theorem".
- Richard Statman. Equality between functionals revisited. Harvey Friedman's research on the foundations of mathematics, pp. 331-338. Studies in logic and the foundations of mathematics 117, North-Holland 1985.