Are the tweaked reduction rules what you have on this website? I might be misunderstanding, but rule 3 certainly looks different on your website than in Barry’s book.

Could you link typed_program_analysis.pdf? I can’t seem to find it.