On the categorical semantics of dependent type theory with function types in locally cartesian closed categories (see at relation between category theory and type theory):
Pierre-Louis Curien, Substitution up to isomorphism, Fundamenta Informaticae, 19 1-2 (1993) 51-86 [doi:10.5555/175469.175471] and: Diagrammes 23 (1990) 43-66 [numdam:DIA_1990__23__43_0]
Pierre-Louis Curien, Richard Garner, Martin Hofmann, Revisiting the categorical interpretation of dependent type theory, Theoretical Computer Science 546 21 (2014) 99-119 [doi:10.1016/j.tcs.2014.03.003, pdf]
On cyclic operads:
Pierre-Louis Curien, Jovana Obradović: A formal language for cyclic operads, Higher Structures 1 1 (2017) 22-55 [arXiv:1602.07502, pdf]
Jovana Obradović: Monoid-like definitions of cyclic operad, Theory and Applications of Categories 32 12 (2017) 396-436 [tac:32-12, pdf]
Pierre-Louis Curien, Jovana Obradović: Categorified cyclic operads, Appl. Categ. Struct. 28 (2020) 59–112 [doi:10.1007/s10485-019-09569-7]
Last revised on April 26, 2026 at 10:27:35. See the history of this page for a list of all contributions to it.