coq translation of Jessie parser, interpreter

agoric-labs / jessica

Jessica - Jessie (secure distributed Javascript) Compiler Architecture

Apache License 2.0

36 stars 9 forks source link

coq translation of Jessie parser, interpreter #52

Open dckc opened 3 years ago

dckc commented 3 years ago

a sort of tooth-brushing idea this morning...

for integration with stuff like HolisticSpecifications

much like the C parser in the seL4 formalization

dckc commented 3 years ago

The interpreter is probably ~10x more work than the parser, but it still seems like straightforward engineering with very little research / design required.

I wonder to what extent the JavaScript standard library has been formalized.

p.s. It's fantastic that the WebAssembly process includes formal specifications.

dckc commented 3 years ago

earlier this week I tried to get started with coq-parsec but I got stuck working out dependencies. I asked for help on parsing, getting started, package dependencies in the coq zulip chat and got some replies but I haven't tried out the suggestions yet.