DOWNLOAD

  1. Lingu. Lingu is a simple language to script database transactions. It is built as an extension of Ecore (below). The logic is implemented, but we still have no execution engine.

    Download: v.4.1 (for HOL K3), v.4 (for HOL K2)

    Installation:

    1. Unzip
    2. in lib/ecore run Holmake clean, then Holmake
    3. in src/lingu run Holmake clean, then Holmake -I ../../lib/ecore

    Report: here (draft)

  2. 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.

  3. Litemech. Litemech is a reincarnation of x-mech (below), built with a better technology. It offers a logic for a simple sequential imperative language. The parser is combinator-based. The logic supports variants for for light weight verification, implemented an Attribute Grammar framework. It has HOL as the back-end prover.

    Download: v.1.3.2, short manual

  4. x-Mech Alpha. This is the first x-Mech prototype, built in the traditional way with YACC-parser and a type-checker coded from scratch. It's provided here mainly for historical purpose. X-Mech Alpha offers a logic for a Promela-like imperative language. It has HOL as the back-end prover.

    Download: v.0.4.