3 ms·

For the HOL family (HOL-light, HOL4, Isabelle/HOL) at least, there is such a VM: OpenTheory (http://opentheory.gilith.com/ http://opentheory.gilith.com/). It's

by c-cube 5y ago

For the HOL family (HOL-light, HOL4, Isabelle/HOL) at least, there is such a VM: OpenTheory (http://opentheory.gilith.com/ http://opentheory.gilith.com/). It's a stack machine with a very simple input format (line based).