FYI there’s an (explicitly interpreted, not proc-encoded) implementation of this in https://computationbook.com, including compilation from lambda calculus: https://github.com/tomstuart/computationbook/tree/master/uni...

And also, as you imply, iota: https://github.com/tomstuart/computationbook/tree/master/uni...