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 problem; Yoneda embedding; extraction of programs from proofs; categories of presheaves; \({\mathcal P}\)-category theory; simply typed \(\lambda\beta\eta\)-calculus
03B70: Logic in computer science
03G30: Categorical logic, topoi
03D40: Word problems, etc. in computability and recursion theory
18F20: Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects)
03B40: Combinatory logic and lambda calculus
Related Items
A general formulation of simultaneous inductive-recursive definitions in type theory, An Isbell duality theorem for type refinement systems, Normalisation of the TheoryTof Cartesian Closed Categories and Conservativity of ExtensionsT[x ofT], Denotational Semantics of Call-by-name Normalization in Lambda-mu Calculus, Coherence for bicategorical cartesian closed structure, CATEGORICAL MODEL CONSTRUCTION FOR PROVING SYNTACTIC PROPERTIES, The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective, Semantic analysis of normalisation by evaluation for typed lambda calculus, Normalization by evaluation and algebraic effects, Category theoretic structure of setoids, The Simple Type Theory of Normalisation by Evaluation, On the Semantics of Intensionality, Formalising Overlap Algebras in Matita
