Normalization and the Yoneda embedding
From MaRDI portal
Publication:4236219
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)
word problemYoneda embeddingextraction of programs from proofscategories of presheaves\({\mathcal P}\)-category theorysimply typed \(\lambda\beta\eta\)-calculus
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
Normalization by evaluation and algebraic effects, Semantic analysis of normalisation by evaluation for typed lambda calculus, Coherence for bicategorical cartesian closed structure, 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
