Deliverable 4

Definition of a mathematical framework for modular reasoning about type theories and their extensions.

Different theories have been developed, some taking a more syntactic approach to the definition of type theories, others a more semantic approach.

• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs, Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna, Journal of Functional Programming, 2021

• Algebraic models of simple type theories: a polynomial approach, Nathanael Arkor, Marcelo Fiore, Logic in Computer Science, 2020

• An extensible equality checking algorithm for dependent type theories, Andrej Bauer, Anja Petkovic Komel, Logical Methods in Computer Science 18(1), 2022.

• Formal metatheory of second-order abstract syntax, Marcelo Fiore, Dmitrij Szamozvancev, Principles Of Programming Languages, 2022

• Implementing a Category-Theoretic Framework for Typed Abstract Syntax, Benedikt Ahrens, Ralph Matthes, Anders Mörtberg, Certified Programs and Proofs, 2022

• Contextual Algebraic Theories: Generic Boilerplate beyond Abstraction (Extended Abstract), Andreas Nuyts, Workshop on Type-Driven Development (TyDe), 2022

• Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses, Taichi Uemura, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023).

• Finitary type theories with and without contexts, Philipp G. Haselwarter, Andrej Bauer, 2023.

• Algebraic presentations of dependent type theories, Benedikt Ahrens, Jacopo Emmenegger, Paige R. North, Egbert Rijke (see also B-systems and C-systems are equivalent)

• For the Metatheory of Type Theory, Internal Sconing Is Enough, Rafaël Bocquet, Ambrus Kaposi, Christian Sattler, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023).

• Type-Theoretic Signatures for Algebraic Theories and Inductive Types, András Kovács, 2023.