User loginNavigation 
Just What is it that Makes MartinLof's Type Theory so Different, so Appealing?MartinLÃ¶f's Type Theory (MLTT) was developed by Per MartinLÃ¶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 propositionsastypes 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 handson stuff... 
Browse archivesActive forum topics

Recent comments
4 hours 39 min ago
2 days 6 hours ago
2 days 7 hours ago
3 days 17 hours ago
3 days 23 hours ago
4 days 9 hours ago
4 days 19 hours ago
4 days 23 hours ago
5 days 5 hours ago
5 days 5 hours ago