A type theory for cartesian closed bicategories:(Extended Abstract)
| Autor: | Marcelo Fiore, Philip Saville |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
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 |
| Zdroj: | 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 |
| DOI: | 10.1109/LICS.2019.8785708 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|