Relative full completeness for bicategorical Cartesian closed structure

DOI10.1007/978-3-030-45231-5_15OpenAlexW3016444786MaRDI QIDQ2200828

Marcelo P. Fiore, Philip Saville

Publication date: 23 September 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-45231-5_15

zbMATH Keywords

rewritingtype theoryconservative extensionbicategoriesglueingCartesian closurerelative full completeness

Mathematics Subject Classification ID

Theory of computing (68Qxx) Theory of software (68Nxx)

Related Items

A categorical framework for congruence of applicative bisimilarity in higher-order languages

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus
• A characterization of lambda definability in categorical models of implicit polymorphism
• Coherence for bicategories and indexed categories
• Cartesian bicategories. I
• A general coherence result
• Introduction to extensive and distributive categories
• Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures
• Remarks on isomorphisms in typed lambda calculi with empty and sum types
• Yoneda structures from 2-toposes
• Cartesian closed 2-categories and permutation equivalence in higher-order rewriting
• A 2-Categories Companion
• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• Cartesian Bicategories II
• Bicategories of spans as cartesian bicategories
• Logical relations and the typed λ-calculus
• Categories for Types
• Games and full completeness for multiplicative linear logic
• Axiomatic Domain Theory in Categories of Partial Maps
• Introduction to bicategories
• The virtues of eta-expansion
• Polynomial functors and polynomial monads
• An abstract formulation for rewrite systems
• Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure
• A Categorical Treatment of Ornaments
• On operads, bimodules and analytic functors
• Games and Strategies as Event Structures
• The cartesian closed bicategory of generalised species of structures
• Iteration 2-theories