natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
As type theory has categorical semantics in 1-categories, 2-type theory has semantics in 2-categories. There are, potentially, many different kinds of “2-type theory” with different uses and semantics. 2-type theory is closely related to (and sometimes the same as) directed type theory?.
The “mode theories” in some general approaches to modal type theory and adjoint type theory are a form of 2-type theory, where the 2-cells represent a general form of “structural rules” acting on modal judgments.
The 2-cells in 2-type theory can also be used to model rewriting, e.g. the process of $\beta$-reduction.
2-type theory, 2-logic
Daniel Licata, Dependently Typed Programming with Domain-Specific Logics PhD Thesis (2011) (pdf) - chapter 7
Dan Licata, Mike Shulman, Adjoint logic with a 2-category of modes, in Logical Foundations of Computer Science 2016 (pdf, slides)
Daniel Licata, Mike Shulman, and Mitchell Riley, A Fibrational Framework for Substructural and Modal Logics (extended version), in Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (doi: 10.4230/LIPIcs.FSCD.2017.25, pdf)
R.A.G. Seely, Modeling computations: a 2-categorical framework pdf
Tom Hirschowitz. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013, 9 (3), pp.10. pdf
Last revised on December 7, 2018 at 02:29:49. See the history of this page for a list of all contributions to it.