…with such an endeavour possibly assisted by:
A Representation of Lambda Terms Suitable for Operations on Their Intensions (Gopalan Nadathur and Debra Sue Wilson.)
https://dl.acm.org/doi/pdf/10.1145/91556.91682
It describes the use of suspensions to delay substitutions in the result of a lambda-abstraction, permitting beta-reductions to be atomic operations.