東北大学 / 大学院情報科学研究科
Formal Verification of the Correspondence between Call-by-Need and Call-by-Name
We formalize the call-by-need evaluation of [equation]-calculus (with no recursive bindings) and prove its correspondence with call-by-name, using the Coq proof assistant. It has been long argued that...