Normalization and the Yoneda embedding

DOI10.1017/S0960129597002508zbMath0918.03012MaRDI QIDQ4236219

Peter Dybjer, Djordje Čubrić, Philip J. Scott

Publication date: 17 August 1999

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

word problemYoneda embeddingextraction of programs from proofscategories of presheaves\({\mathcal P}\)-category theorysimply typed \(\lambda\beta\eta\)-calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Categorical logic, topoi (03G30) Word problems, etc. in computability and recursion theory (03D40) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Combinatory logic and lambda calculus (03B40)

Related Items (14)

Normalization by evaluation and algebraic effects ⋮ Semantic analysis of normalisation by evaluation for typed lambda calculus ⋮ Coherence for bicategorical cartesian closed structure ⋮ Embeddability of ptykes ⋮ On the Semantics of Intensionality ⋮ An Isbell duality theorem for type refinement systems ⋮ The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective ⋮ Category theoretic structure of setoids ⋮ Normalisation of the TheoryTof Cartesian Closed Categories and Conservativity of ExtensionsT[x ofT] ⋮ Formalising Overlap Algebras in Matita ⋮ Denotational Semantics of Call-by-name Normalization in Lambda-mu Calculus ⋮ The Simple Type Theory of Normalisation by Evaluation ⋮ CATEGORICAL MODEL CONSTRUCTION FOR PROVING SYNTACTIC PROPERTIES ⋮ A general formulation of simultaneous inductive-recursive definitions in type theory

This page was built for publication: Normalization and the Yoneda embedding