3 ms·
The most influential paper (Bob Harper): Per Martin-Löf: Constructive Mathematics and Computer Programming https://www.cs.tufts.edu/~nr/cs257/archive/per-mart
by hackandthink 4y ago
The most influential paper (Bob Harper):
Per Martin-Löf: Constructive Mathematics and Computer Programming
https://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf https://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/co...
- 082349872349872 4y ago> The transfinite recursion form (Tx,y , z)(c, d) has not yet found any applications in programming. Has it found any applications in the intervening 40 years? Edit: a more approachable exposition is on p43+ of https://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/ITT.pdf https://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/IT...
- hackandthink 4y agoThanks I guess Martin-Löf speaks about W-Types. An implementation and examples in Coq: https://github.com/coq/coq/wiki/WTypeInsteadOfInductiveTypes https://github.com/coq/coq/wiki/WTypeInsteadOfInductiveTypes Still waiting for the year of W-Types