Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

B.P. Ahrens; Peter LeFanu Lumsdaine; P.R. North

doi:10.1007/978-981-97-8943-6_1

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

B.P. Ahrens^*, Peter LeFanu Lumsdaine, P.R. North

^*Corresponding author for this work

Programming Languages

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

Abstract

Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take comprehension categories as a unifying language, and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.

Original language	English
Title of host publication	Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings
Subtitle of host publication	22nd Asian Symposium, APLAS 2024, Proceedings
Editors	Oleg Kiselyov
Publisher	Springer
Pages	3-22
Number of pages	20
ISBN (Electronic)	978-981-97-8943-6
ISBN (Print)	978-981-97-8942-9
DOIs	https://doi.org/10.1007/978-981-97-8943-6_1
Publication status	Published - 2024
Event	22nd Asian Symposium on Programming Languages and Systems - Kyoto, Japan Duration: 22 Oct 2024 → 24 Oct 2024 Conference number: 22

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	15194 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd Asian Symposium on Programming Languages and Systems
Abbreviated title	APLAS 2024
Country/Territory	Japan
City	Kyoto
Period	22/10/24 → 24/10/24

Bibliographical note

Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – Taverne project https://www.openaccess.nl/en/you-share-we-take-care
Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public.

Keywords

dependent types
categorical semantics

Access to Document

10.1007/978-981-97-8943-6_1

978-981-97-8943-6_1Final published version, 663 KB

Cite this

Ahrens, B. P., LeFanu Lumsdaine, P., & North, P. R. (2024). Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. In O. Kiselyov (Ed.), Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings: 22nd Asian Symposium, APLAS 2024, Proceedings (pp. 3-22). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 15194 LNCS). Springer. https://doi.org/10.1007/978-981-97-8943-6_1

Ahrens, B.P. ; LeFanu Lumsdaine, Peter ; North, P.R. / Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings: 22nd Asian Symposium, APLAS 2024, Proceedings. editor / Oleg Kiselyov. Springer, 2024. pp. 3-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{b8cc1197a0864b7bb9876dbefc1ca304,

title = "Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories",

abstract = "Algebraic theories with dependency between sorts form the structural core of Martin-L{\"o}f type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take comprehension categories as a unifying language, and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.",

keywords = "dependent types, categorical semantics",

author = "B.P. Ahrens and {LeFanu Lumsdaine}, Peter and P.R. North",

note = "Green Open Access added to TU Delft Institutional Repository {\textquoteleft}You share, we take care!{\textquoteright} – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public. ; 22nd Asian Symposium on Programming Languages and Systems, APLAS 2024 ; Conference date: 22-10-2024 Through 24-10-2024",

year = "2024",

doi = "10.1007/978-981-97-8943-6_1",

language = "English",

isbn = "978-981-97-8942-9",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "3--22",

editor = "Oleg Kiselyov",

booktitle = "Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings",

}

Ahrens, BP, LeFanu Lumsdaine, P & North, PR 2024, Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. in O Kiselyov (ed.), Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings: 22nd Asian Symposium, APLAS 2024, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 15194 LNCS, Springer, pp. 3-22, 22nd Asian Symposium on Programming Languages and Systems, Kyoto, Japan, 22/10/24. https://doi.org/10.1007/978-981-97-8943-6_1

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. / Ahrens, B.P.; LeFanu Lumsdaine, Peter; North, P.R.
Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings: 22nd Asian Symposium, APLAS 2024, Proceedings. ed. / Oleg Kiselyov. Springer, 2024. p. 3-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 15194 LNCS).

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

TY - GEN

T1 - Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

AU - Ahrens, B.P.

AU - LeFanu Lumsdaine, Peter

AU - North, P.R.

N1 - Conference code: 22

PY - 2024

Y1 - 2024

N2 - Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take comprehension categories as a unifying language, and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.

AB - Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take comprehension categories as a unifying language, and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.

KW - dependent types

KW - categorical semantics

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

U2 - 10.1007/978-981-97-8943-6_1

DO - 10.1007/978-981-97-8943-6_1

M3 - Conference contribution

SN - 978-981-97-8942-9

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 22

BT - Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings

A2 - Kiselyov, Oleg

PB - Springer

T2 - 22nd Asian Symposium on Programming Languages and Systems

Y2 - 22 October 2024 through 24 October 2024

ER -

Ahrens BP, LeFanu Lumsdaine P, North PR. Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. In Kiselyov O, editor, Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings: 22nd Asian Symposium, APLAS 2024, Proceedings. Springer. 2024. p. 3-22. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-981-97-8943-6_1

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this