We give a new characterisation of morphisms that are definable by the interpretation of the simply typed lambda calculus with sums in any bi-Cartesian closed category. The ⊤ ⊤-closure operator will be used to construct the category in which the collection of definable morphisms at sum types can be characterised as the coproducts of such collections at lower types.
CITATION STYLE
Katsumata, S. (2008). A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators. In Computer Science Logic (pp. 278–292). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-87531-4_21
Mendeley helps you to discover research relevant for your work.