## User login## Navigation |
## Just What is it that Makes Martin-Lof's Type Theory so Different, so Appealing?Martin-LÃ¶f's Type Theory (M-LTT) was developed by Per Martin-LÃ¶f in the early 1970s, as a constructive foundation for mathematics. The theory is clear and simple. Because of this it has been used for everything from program derivation to handling donkey sentences. Yet another propositions-as-types tutorial. It seems pretty easy to follow, and it is quite short (16 pages). P.S Why all the theory on LtU these days? Because the editors who keep posting are into theory. The other editors should be nudged to start posting cool hands-on stuff... |
## Browse archives
## Active forum topics |

## Recent comments

5 weeks 2 days ago

5 weeks 2 days ago

5 weeks 2 days ago

27 weeks 3 days ago

31 weeks 5 days ago

33 weeks 2 days ago

33 weeks 2 days ago

36 weeks 15 hours ago

40 weeks 5 days ago

40 weeks 5 days ago