Semantics for two-dimensional type theory

Benedikt Ahrens; Paige Randall North; Niels Van Der Weide

doi:10.1145/3531130.3533334

Semantics for two-dimensional type theory

Benedikt Ahrens, Paige Randall North, Niels Van Der Weide

Computer Science

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

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	LICS '22
Subtitle of host publication	Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
Publisher	Association for Computing Machinery (ACM)
ISBN (Electronic)	9781450393515
DOIs	https://doi.org/10.1145/3531130.3533334
Publication status	Published - 4 Aug 2022
Event	37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) - Technion, Haifa, Israel Duration: 2 Aug 2022 → 5 Aug 2022

Publication series

Name	LICS: Logic in Computer Science

Conference

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

Bibliographical note

Acknowledgments:
We gratefully acknowledge the work by the Coq development team in providing the Coq proof assistant and surrounding infrastructure, as well as their support in keeping UniMath compatible with Coq. We are very grateful to Dan Licata and Bob Harper for their help in understanding their interpretation and how it fits into our framework. We thank the anonymous referees for their insightful comments. This work was partially funded by EPSRC under agreement number EP/T000252/1. This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0334.

Keywords

directed type theory
dependent types
comprehension bicategory
computer-checked proof

Access to Document

10.1145/3531130.3533334Licence: Creative Commons: Attribution (CC BY)

AhrensB2022SemanticsFinal published version, 1.57 MBLicence: Creative Commons: Attribution (CC BY)

A theory of type theories
Ahrens, B.
Engineering & Physical Science Research Council
1/03/20 → 31/08/22
Project: Research Councils

Cite this

@inproceedings{97b57108a0404d26b3e20507e3bf6924,

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 North, {Paige Randall} and {Van Der Weide}, Niels",

note = "Acknowledgments: We gratefully acknowledge the work by the Coq development team in providing the Coq proof assistant and surrounding infrastructure, as well as their support in keeping UniMath compatible with Coq. We are very grateful to Dan Licata and Bob Harper for their help in understanding their interpretation and how it fits into our framework. We thank the anonymous referees for their insightful comments. This work was partially funded by EPSRC under agreement number EP/T000252/1. This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0334. ; 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), LICS 2022 ; Conference date: 02-08-2022 Through 05-08-2022",

year = "2022",

month = aug,

day = "4",

doi = "10.1145/3531130.3533334",

language = "English",

series = "LICS: Logic in Computer Science",

publisher = "Association for Computing Machinery (ACM)",

booktitle = "LICS '22",

address = "United States",

}

Ahrens, B, North, PR & Van Der Weide, N 2022, Semantics for two-dimensional type theory. in LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, Association for Computing Machinery (ACM), 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Haifa, Israel, 2/08/22. https://doi.org/10.1145/3531130.3533334

TY - GEN

T1 - Semantics for two-dimensional type theory

AU - Ahrens, Benedikt

AU - North, Paige Randall

AU - Van Der Weide, Niels

N1 - Acknowledgments: We gratefully acknowledge the work by the Coq development team in providing the Coq proof assistant and surrounding infrastructure, as well as their support in keeping UniMath compatible with Coq. We are very grateful to Dan Licata and Bob Harper for their help in understanding their interpretation and how it fits into our framework. We thank the anonymous referees for their insightful comments. This work was partially funded by EPSRC under agreement number EP/T000252/1. This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0334.

PY - 2022/8/4

Y1 - 2022/8/4

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

U2 - 10.1145/3531130.3533334

DO - 10.1145/3531130.3533334

M3 - Conference contribution

T3 - LICS: Logic in Computer Science

BT - LICS '22

PB - Association for Computing Machinery (ACM)

T2 - 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Y2 - 2 August 2022 through 5 August 2022

ER -

Semantics for two-dimensional type theory

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Fingerprint

Projects

A theory of type theories

Cite this