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

1 hour 33 min ago

11 hours 52 min ago

3 days 8 hours ago

4 days 5 hours ago

2 weeks 23 hours ago

2 weeks 1 day ago

2 weeks 1 day ago

2 weeks 1 day ago

2 weeks 1 day ago

3 weeks 4 hours ago