東北大学 / 大学院情報科学研究科
Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion
We present new proofs—formalized in the Coq proof assistant—of the correspondence among call-by-need and (various definitions of) call-by-name evaluations of [equation]-calculus with mutually...