Zulip Chat Archive

Stream: general

Topic: Computational interpretation

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 ?

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

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: Dec 20 2023 at 11:08 UTC