A type theory for cartesian closed bicategories
- Submitting institution
-
University of Cambridge
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1883
- Type
- E - Conference contribution
- DOI
-
10.1109/LICS.2019.8785708
- Title of conference / published proceedings
- 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
- First page
- 1
- Volume
- 00
- Issue
- -
- ISSN
- 1043-6871
- Open access status
- Compliant
- Month of publication
- August
- Year of publication
- 2019
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
0
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- A central methodological contribution of the paper is the design of a 2-dimensional type theory (of typed terms and rewrites between them) from mathematical principles arising from the concept of bicategorical adjunction as expressed by the notion of biuniversal arrow. The upshot of the work is a 2-dimensional extension of the fundamental Curry-Howard-Lambek correspondence in logic, type theory, and category theory.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -