A type theory for cartesian closed bicategories: (Extended Abstract)

Marcelo Fiore; Philip Saville

doi:10.1109/LICS.2019.8785708

A type theory for cartesian closed bicategories: (Extended Abstract)

Marcelo Fiore, Philip Saville

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English
Title of host publication	2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Subtitle of host publication	24-27 June 2019 - Vancouver
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	1-13
Number of pages	13
ISBN (Electronic)	978-1-7281-3608
ISBN (Print)	978-1-7281-3609-7
DOIs	https://doi.org/10.1109/LICS.2019.8785708
Publication status	Published - 5 Aug 2019
Event	Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science - Vancouver, Canada Duration: 24 Jun 2019 → 27 Jun 2019 http://lics.siglog.org/lics19/index.php

Conference

Conference	Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS 2019
Country/Territory	Canada
City	Vancouver
Period	24/06/19 → 27/06/19
Internet address	http://lics.siglog.org/lics19/index.php

Keywords

typed lambda calculus
higher category theory
Curry-Howard-Lambek correspondence
cartesian closed bicategories

Access to Document

10.1109/LICS.2019.8785708Licence: All Rights Reserved

A type theory_FIORE_DoA290319_AFVAccepted author manuscript, 330 KB

https://ieeexplore.ieee.org/document/8785708Licence: All Rights Reserved

1 Abstract

A type theory for cartesian closed bicategories
Saville, P. & Fiore, M., 9 Jul 2019. 1 p.
Research output: Contribution to conference › Abstract

Open Access

2 Invited talk

Coherence through normalisation-by-evaluation for cartesian closed bicategories
Philip Saville (Invited speaker) & Marcelo Fiore (Contributor)
12 Nov 2019
Activity: Academic talk or presentation types › Invited talk
A type theory for cartesian closed bicategories
Philip Saville (Invited speaker) & Marcelo Fiore (Contributor)
8 May 2019
Activity: Academic talk or presentation types › Invited talk

Cite this

@inproceedings{a9a7232b27b44a66908d29ea56a72fa7,

title = "A type theory for cartesian closed bicategories: (Extended Abstract)",

abstract = "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. ",

keywords = "typed lambda calculus, higher category theory, Curry-Howard-Lambek correspondence, cartesian closed bicategories",

author = "Marcelo Fiore and Philip Saville",

year = "2019",

month = aug,

day = "5",

doi = "10.1109/LICS.2019.8785708",

language = "English",

isbn = "978-1-7281-3609-7",

pages = "1--13",

booktitle = "2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

address = "United States",

note = "Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019 ; Conference date: 24-06-2019 Through 27-06-2019",

url = "http://lics.siglog.org/lics19/index.php",

}

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

TY - GEN

T1 - A type theory for cartesian closed bicategories

T2 - Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science

AU - Fiore, Marcelo

AU - Saville, Philip

PY - 2019/8/5

Y1 - 2019/8/5

N2 - 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.

AB - 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.

KW - typed lambda calculus

KW - higher category theory

KW - Curry-Howard-Lambek correspondence

KW - cartesian closed bicategories

U2 - 10.1109/LICS.2019.8785708

DO - 10.1109/LICS.2019.8785708

M3 - Conference contribution

SN - 978-1-7281-3609-7

SP - 1

EP - 13

BT - 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

PB - Institute of Electrical and Electronics Engineers (IEEE)

Y2 - 24 June 2019 through 27 June 2019

ER -

A type theory for cartesian closed bicategories: (Extended Abstract)

Abstract

Conference

Keywords

Access to Document

Fingerprint

Research output

A type theory for cartesian closed bicategories

Activities

Coherence through normalisation-by-evaluation for cartesian closed bicategories

A type theory for cartesian closed bicategories

Cite this