News for hackers. Stuff that matters.

A comment on Kind: A Modern Proof Language. Parent comment

Re:Kind: A Modern Proof Language by c-cube on Wednesday August 11, 2021 @12:26PM (#28144118)
For the HOL family (HOL-light, HOL4, Isabelle/HOL) at least, there is such a VM: OpenTheory (http://opentheory.gilith.com/). It's a stack machine with a very simple input format (line based).
[ Parent | on HN ]

There are no comments on this comment yet.