HVM semantics (in Maude)

[crides]

Hi! I decided that as part of a class project, I would write out the semantics of HVM in the Maude term rewriting system. This is both because I think HVM is a very interesting project, and I don't quite understand how it works (maybe implementing the semantics would help with that). I'm only just getting started, and have just done number duping and working on constructor duping.

I mainly want to ask what kind of resources I can use for this. I'm currently going off of HOW.md as it seems to have all (most?) of the main reduction rules, and using the old (v0.1.89) implementation to check (as it prints out the exact rewrites to get to the result). Are these still good references? Or are there other important bits that are not documented and I need to read the implementation? Which version is better?

I've also skimmed papers/articles/documents linked around the repo. They are definitely useful for understanding how SIC works, though I'm not sure yet how far that is from HVM itself.

Thanks in advance!

[Boscop]

Writing the semantics in Maude sounds like an interesting project.
Btw, were you already aware of this document? https://github.com/HigherOrderCO/Wikind/blob/master/IC/_.kind2
There is also a lot of detail here: https://github.com/HigherOrderCO/HVM/blob/master/src/runtime/base/memory.rs

[crides]

I probably didn't see it when I posted, but I did find it afterwards. Looking at it now, the formulation in kind2 helps a bit more than the rewrite rules provided as comments in the source. The lower level implementation details are interesting, but for now I'm just focusing on the parts from syntax to SIC rules.

[crides]

The (S)IC implementation is pretty helpful. The semester has ended, and I have my current progress here: https://github.com/crides/hvm-maude