Semantics for two-dimensional type theory

Benedikt  Ahrens; P.R. North; Niels  van der Weide

doi:10.1145/3531130.3533334

Semantics for two-dimensional type theory

Benedikt Ahrens, P.R. North, Niels van der Weide

Programming Languages

Research output: Chapter in Book/Conference proceedings/Edited volume › Conference contribution › Scientific › peer-review

3 Citations (Scopus)

94 Downloads (Pure)

Abstract

We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature. From comprehension bicategories, we extract a core syntax, that is, judgment forms and structural inference rules, for a two-dimensional type theory. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library. This work is the first step towards a theory of syntax and semantics for higher-dimensional directed type theory.

Original language	English
Title of host publication	Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022
Place of Publication	New York
Publisher	ACM
Number of pages	14
ISBN (Print)	978-1-4503-9351-5
DOIs	https://doi.org/10.1145/3531130.3533334
Publication status	Published - 2022
Event	37th Annual ACM/IEEE Symposium on Logic in Computer Science - Haifa, Israel Duration: 2 Aug 2022 → 5 Aug 2022 Conference number: 27

Conference

Conference	37th Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS ’22
Country/Territory	Israel
City	Haifa
Period	2/08/22 → 5/08/22

Keywords

directed type theory
dependent types
comprehension bicategory,
computer-checked proof

Access to Document

10.1145/3531130.3533334

3531130.3533334Final published version, 1.54 MBLicence: CC BY

Cite this

@inproceedings{7b774bd097774a649eabc9699ea99c06,

title = "Semantics for two-dimensional type theory",

abstract = "We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature. From comprehension bicategories, we extract a core syntax, that is, judgment forms and structural inference rules, for a two-dimensional type theory. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library. This work is the first step towards a theory of syntax and semantics for higher-dimensional directed type theory. ",

keywords = "directed type theory, dependent types, comprehension bicategory,, computer-checked proof",

author = "Benedikt Ahrens and P.R. North and {van der Weide}, Niels",

year = "2022",

doi = "10.1145/3531130.3533334",

language = "English",

isbn = "978-1-4503-9351-5",

booktitle = "Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022",

publisher = "ACM",

address = "United States",

note = "37th Annual ACM/IEEE Symposium<br/>on Logic in Computer Science, LICS {\textquoteright}22 ; Conference date: 02-08-2022 Through 05-08-2022",

}

TY - GEN

T1 - Semantics for two-dimensional type theory

AU - Ahrens, Benedikt

AU - North, P.R.

AU - van der Weide, Niels

N1 - Conference code: 27

PY - 2022

Y1 - 2022

N2 - We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature. From comprehension bicategories, we extract a core syntax, that is, judgment forms and structural inference rules, for a two-dimensional type theory. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library. This work is the first step towards a theory of syntax and semantics for higher-dimensional directed type theory.

AB - We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature. From comprehension bicategories, we extract a core syntax, that is, judgment forms and structural inference rules, for a two-dimensional type theory. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library. This work is the first step towards a theory of syntax and semantics for higher-dimensional directed type theory.

KW - directed type theory

KW - dependent types

KW - comprehension bicategory,

KW - computer-checked proof

UR - http://www.scopus.com/inward/record.url?scp=85136949817&partnerID=8YFLogxK

U2 - 10.1145/3531130.3533334

DO - 10.1145/3531130.3533334

M3 - Conference contribution

SN - 978-1-4503-9351-5

BT - Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022

PB - ACM

CY - New York

T2 - 37th Annual ACM/IEEE Symposium<br/>on Logic in Computer Science

Y2 - 2 August 2022 through 5 August 2022

ER -

Semantics for two-dimensional type theory

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this