## 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## New forum topics |

## Recent comments

5 days 5 hours ago

5 days 11 hours ago

6 days 5 hours ago

1 week 18 hours ago

1 week 6 days ago

2 weeks 9 hours ago

2 weeks 18 hours ago

2 weeks 1 day ago

2 weeks 5 days ago

3 weeks 19 hours ago