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
The notion of M-type is the formal dual of that of W-type: a certain coinductive type.
The categorical semantics of an $M$-type is a terminal coalgebra of an endofunctor.
Benno van den Berg, de Marchi Non-well-founded trees in categories, APAL 146 (2007) 40–59.
Benedikt Ahrens, Paolo Capriotti and Régis Spadotti, Non-wellfounded trees in Homotopy Type Theory, link
Andrea Vezzosi, On Induction, Coinduction and Equality in Martin-Löf and Homotopy Type Theory thesis
R.E. Møgelberg, N. Veltri, Bisimulation as path type for guarded recursive types POPL 2019. arXiv
Last revised on February 17, 2019 at 09:26:54. See the history of this page for a list of all contributions to it.