Jonathan Gallagher

Title: A tutorial on the Scott–Koymans [*] theorem part 2
Abstract: We will continue our investigation into the modernization of the Scott-Koymans theorem. This theorem says, roughly, that the semantics of the untyped lambda calculus into CCCs with a reflexive object, is sound and complete — in fact it says:
Theorem: Every lambda theory T, has a model M, whose theory is equivalent to T. Moroever, these models are always are given by a reflexive object in a CCC.
Last time we stopped at the definition of the category of lambda theories. This time we will continue the investigation by considering the “semantic part”, and move towards constructing the adjunction between syntax and semantics.
 
Footnote:
Really,
[*] = [1-5]
1) Scott (`80) “Relating theories of the lambda calculus”
2) Hindey and Longo (`80) “Lambda-calculus models and extensionality”
3) Meyer (`82) “What is a model of the lambda calculus?”
4) Barendregt and Koymans (`80) “Comparing some classes of lambda calculus
models”
5) Koymans (`82) “Models of the lambda calculus”