In the article at nlab about the relation between type theory and category theory, it is said that "beta reduction" in type theory corresponds to "counit for hom-tensor adjunction" in category theory and also "substitution" corresponds to "composition of classifying morphisms / pullback of display maps" correspondingly.

Are these considered denotational or operational semantics?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.