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/co...
back
1 comments
> 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/IT...
Thanks
I guess Martin-Löf speaks about W-Types.
An implementation and examples in Coq:
https://github.com/coq/coq/wiki/WTypeInsteadOfInductiveTypes
Still waiting for the year of W-Types