Even if I'am far from understand your paper in deep, I like the way you explore new ways in lambda-calculus, mainly I think following John Tromp's works. I'm exploring lambda-calculus with binary numbers of any size using a home-made language, http://lambdaway.free.fr/lambdawalks, in this wiki page, http://lambdaway.free.fr/lambdawalks/?view=oops6, and it's funny. Your work is inspiring. Thank you.