Ecore. Ecore is a reincarnation of litemech (below). It offers a logic
for a simple sequential imperative language called L0. It is implemented via syntactical
embedding in HOL. This implementation is much lighter than litemech, because we
can reuse HOL's own parser and type checker. However, the concrete syntax of L0
is not as nice as Litemech. L0 features block, program call, pass-by-value and
pass-by-reference parameters, return value, and "old" key-word in the specification
to refer to a variable's initial value, and a language TEST to specify unit tests. L0
is also underspecified in some places, allowing some
room for customization.
Download:
v1 (for HOL K3),
v0 (for HOL K2).
Installation: Unzip, run Holmake clean, then Holmake.