Coherence and normalisation-by-evaluation for bicategorical Cartesian closed structure

DOI10.1145/3373718.3394769MaRDI QIDQ5145652zbMATH OpenOpenAlexFDO

Authors Philip Saville, Marcelo P. Fiore

Publication date 21 January 2021

Published in Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3373718.3394769

zbMATH Keywords

bicategoriesCartesian closurecoherencenormalisationnormalisation-by-evaluationtype theory

Mathematics Subject Classification ID

Type theory (03B38) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) 2-categories, bicategories, double categories (18N10)

Recommendations

• Coherence for bicategorical cartesian closed structure
• Bicartesian coherence
• Coherence in Cartesian closed categories and the generality of proofs
• Applications of methods of proof theory in category theory.
• Coherence for closed categories with biproducts

Cited in

(6)

• Bicartesian coherence
• Relative full completeness for bicategorical Cartesian closed structure
• A categorical framework for congruence of applicative bisimilarity in higher-order languages
• Coherence for bicategorical cartesian closed structure
• A type theory for Cartesian closed bicategories
• Coherence by normalization for linear multicategorical structures

This page was built for publication: Coherence and normalisation-by-evaluation for bicategorical Cartesian closed structure

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145652)