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
abstract duality: opposite category,
concrete duality: dual object, dualizable object, fully dualizable object, dualizing object
between higher geometry/higher algebra
Langlands duality, geometric Langlands duality, quantum geometric Langlands duality
Adjoint logic or adjoint type theory is formal logic or type theory which natively expresses adjunctions of modal operators, adjoint modalities.
Nick Benton, Philip Wadler, Linear logic, monads and the lambda calculus, In IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1996.
Jason Reed, A judgemental deconstruction of modal logic, 2009, (pdf)
Klaas Pruiksma, William Chargin, Frank Pfenning, and Jason Reed, Adjoint Logic, 2018, (pdf)
A framework for (homotopy-)type theoretic adjoint logic (modal type theory) is discussed, in various stages of generality, in
Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)
(specifically for cohesive homotopy type theory)
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)
(for modal simple type theory)
Review includes
Last revised on January 7, 2019 at 21:10:30. See the history of this page for a list of all contributions to it.