Researchers map hidden structure of advanced programming languages
Computer scientists have created a unified framework for understanding different mathematical models used to build modern programming languages and type systems. The work addresses a 30-year gap in the field by showing how competing approaches actually fit together—a finding that could simplify how language designers build more reliable software tools.
Originaltitel: Comparing semantic frameworks for dependently-sorted algebraic theories
<p>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.</p><p>We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take <em>comprehension categories</em> 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.</p>