You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We should write a compiler of Lean to the EVM. The best approach seems to be compiling it to Yul instead of the EVM directly. Yul is a first order language without function pointers and no jumps. To compile a higher-order program will then require us to write a function dispatcher. Thankfully, the paper on GRIN describes a way to make this efficient. The other things we have to consider is how objects (including closures) should be represented in memory so we can devise an allocator and a collector (which could be just refcounting)
The text was updated successfully, but these errors were encountered:
We should write a compiler of Lean to the EVM. The best approach seems to be compiling it to Yul instead of the EVM directly. Yul is a first order language without function pointers and no jumps. To compile a higher-order program will then require us to write a function dispatcher. Thankfully, the paper on GRIN describes a way to make this efficient. The other things we have to consider is how objects (including closures) should be represented in memory so we can devise an allocator and a collector (which could be just refcounting)
The text was updated successfully, but these errors were encountered: