『「単一代入」と「末尾再帰」』

数理科学的バグ撲滅方法論のすすめ - 第2回 「単一代入」と「末尾再帰」：ITpro
IT Pro連載第2回 - sumiiの日記

ACL2の通常モードだとループが全く書けないのにむかついていたのですが、これを見てなんとなく納得できました。住井さん、ありがとうございます。