Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

Benedikt Ahrens; Peter LeFanu  Lumsdaine; Paige Randall North

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

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

Benedikt Ahrens^*, Peter LeFanu Lumsdaine, Paige Randall North

^*Corresponding author for this work

Computer Science

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

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
Subtitle of host publication	22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings
Editors	Oleg Kiselyov
Publisher	Springer
Pages	3-22
Number of pages	20
Edition	1
ISBN (Electronic)	9789819789436
ISBN (Print)	9789819789429
DOIs	https://doi.org/10.1007/978-981-97-8943-6_1
Publication status	Published - 28 Oct 2024
Event	The 22nd Asian Symposium on Programming Languages and Systems - Kyoto, Japan Duration: 22 Oct 2024 → 24 Oct 2024

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	15194
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

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

Access to Document

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

AhrensB2024Comparing_AAM
This version of the contribution has been accepted for publication, after peer review (when applicable) but is not the Version of Record and does not reflect post-acceptance improvements, or any corrections. The Version of Record is available online at: https://doi.org/10.1007/978-981-97-8943-6_1]. Use of this Accepted Version is subject to the publisher’s Accepted Manuscript terms of use https://www.springernature.com/gp/open-research/policies/accepted-manuscript-terms
Accepted author manuscript, 326 KBLicence: Other (please specify with Rights Statement)

Cite this

Ahrens, B., Lumsdaine, P. L., & 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, Kyoto, Japan, October 22-24, 2024, Proceedings (1 ed., pp. 3-22). (Lecture Notes in Computer Science; Vol. 15194). Springer. https://doi.org/10.1007/978-981-97-8943-6_1

@inproceedings{13c1f9af1fc14a61b7a2c47fc44b72ee,

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

author = "Benedikt Ahrens and Lumsdaine, \{Peter LeFanu\} and North, \{Paige Randall\}",

year = "2024",

month = oct,

day = "28",

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

language = "English",

isbn = "9789819789429",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "3--22",

editor = "Oleg Kiselyov",

booktitle = "Programming Languages and Systems",

edition = "1",

note = "The 22nd Asian Symposium on Programming Languages and Systems, APLAS 2024 ; Conference date: 22-10-2024 Through 24-10-2024",

}

Ahrens, B, Lumsdaine, PL & North, PR 2024, Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. in O Kiselyov (ed.), Programming Languages and Systems : 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings. 1 edn, Lecture Notes in Computer Science, vol. 15194, Springer, pp. 3-22, The 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, Benedikt; Lumsdaine, Peter LeFanu ; North, Paige Randall.
Programming Languages and Systems : 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings. ed. / Oleg Kiselyov. 1. ed. Springer, 2024. p. 3-22 (Lecture Notes in Computer Science; Vol. 15194).

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

TY - GEN

T1 - Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

AU - Ahrens, Benedikt

AU - Lumsdaine, Peter LeFanu

AU - North, Paige Randall

PY - 2024/10/28

Y1 - 2024/10/28

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.

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

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

M3 - Conference contribution

SN - 9789819789429

T3 - Lecture Notes in Computer Science

SP - 3

EP - 22

BT - Programming Languages and Systems

A2 - Kiselyov, Oleg

PB - Springer

T2 - The 22nd Asian Symposium on Programming Languages and Systems

Y2 - 22 October 2024 through 24 October 2024

ER -

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this