Zulip Chat Archive

Stream: general

Topic: Computational interpretation


view this post on Zulip Bas Spitters (Mar 28 2020 at 09:54):

Question at the HoTT zulip. What is the computational interpretation of lean? I understand it's a VM that is currently in flux.
What's the latest on this? @Mario Carneiro ?

view this post on Zulip Mario Carneiro (Mar 28 2020 at 09:58):

The VM has a well defined operational semantics. It is not documented, but there are no issues with it AFAIK

view this post on Zulip Mario Carneiro (Mar 28 2020 at 09:58):

lean 4 adds a bunch of stuff but I don't think the operational semantics have changed in any meaningful way


Last updated: May 13 2021 at 18:26 UTC