A type theory for cartesian closed bicategories:(Extended Abstract)
| العنوان: | A type theory for cartesian closed bicategories:(Extended Abstract) |
|---|---|
| المؤلفون: | Marcelo Fiore, Philip Saville |
| المصدر: | Fiore, M & Saville, P 2019, A type theory for cartesian closed bicategories : (Extended Abstract) . in 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) : 24-27 June 2019-Vancouver . Institute of Electrical and Electronics Engineers (IEEE), pp. 1-13, Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science, Vancouver, Canada, 24/06/19 . https://doi.org/10.1109/LICS.2019.8785708 LICS |
| بيانات النشر: | Institute of Electrical and Electronics Engineers (IEEE), 2019. |
| سنة النشر: | 2019 |
| مصطلحات موضوعية: | typed lambda calculus, Computer science, 010102 general mathematics, cartesian closed bicategories, Substitution (algebra), Curry-Howard-Lambek correspondence, 0102 computer and information sciences, Bicategory, 01 natural sciences, Algebra, Cartesian closed category, Type theory, Explicit substitution, 010201 computation theory & mathematics, Mathematics::Category Theory, Computer Science::Logic in Computer Science, higher category theory, Universal algebra, Computer Science::Programming Languages, Universal property, 0101 mathematics, Lambda calculus, computer, computer.programming_language |
| الوصف: | We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that its syntactic model satisfies an appropriate universal property, thereby lifting the Curry-Howard-Lambek correspondence to the bicategorical setting. Our approach is principled and practical. Weak substitution structure is constructed using a bicategorification of the notion of abstract clone from universal algebra, and the rules for products and exponentials are synthesised from semantic considerations. The result is a type theory that employs a novel combination of 2-dimensional type theory and explicit substitution, and directly generalises the Simply-Typed Lambda Calculus. This work is the first step in a programme aimed at proving coherence for cartesian closed bicategories. |
| وصف الملف: | application/pdf |
| اللغة: | English |
| DOI: | 10.1109/LICS.2019.8785708 |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_dedup___::33e63ff1b8118b2534de1d297edd8e3f https://hdl.handle.net/20.500.11820/a9a7232b-27b4-4a66-908d-29ea56a72fa7 |
| Rights: | OPEN |
| رقم الانضمام: | edsair.doi.dedup.....33e63ff1b8118b2534de1d297edd8e3f |
| قاعدة البيانات: | OpenAIRE |
| DOI: | 10.1109/LICS.2019.8785708 |
|---|