## 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

3 hours 57 min ago

8 hours 42 min ago

1 day 8 hours ago

1 day 10 hours ago

1 day 16 hours ago

2 days 9 hours ago

2 days 18 hours ago

3 days 5 hours ago

3 days 6 hours ago

3 days 6 hours ago