User loginNavigation |
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
4 days 11 hours ago
40 weeks 6 days ago
40 weeks 6 days ago
40 weeks 6 days ago
1 year 10 weeks ago
1 year 15 weeks ago
1 year 16 weeks ago
1 year 16 weeks ago
1 year 19 weeks ago
1 year 24 weeks ago