Sorry I wasn't clear - beta-reduction is formal, I was trying to refer to the extension of the formal treatment of lambdas to cover proofs, formal logic and typechecking. Shen does this for typechecking.