I've noted that both Martin-Lof type theory and [Weak] Monadic Second-Order logic (eg over trees) enjoy the ability to express basically any finite computer program, in a decidable manner. I was wondering how can one compare those two systems. I understand that MLTT lets you use dependent types and by that easily express quite complicated structures, but I'm more interested in the logical properties: for example, are there things that are decidable under MSOL over trees while their equivalent representation in MLTT will lead to undecidability, or vice versa?reference for decidable MSOL over trees: http://www.cs.ox.ac.uk/people/luke.ong/personal/publications/lics06.pdf
MLTT vs. [weak] MSOL
lo.logic;type theory