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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.