Semantics of the typed -calculus with substitution in a cartesian closed category
Résumé
Two versions of semantics of the typed l-calculus with substitution are given. The first uses a global environments object which is the domain of all interpreted terms, while the second uses individual environments objects for each term. The algebraic properties of the environments object(s) play a central role in showing that the interpretation function is invariant under the operational semantics given by substitution.