MEngine is a dependently typed kernel with explicit context management, a proof engine, a tactic language, and a theorem prover, optimized for highly automated proof scripts.
The original ideas and design of MEngine were detailed in my master's thesis1, but have since been refined.
MEngine represents proof terms as λ-DAGs 2: directed acyclic graphs where subterms are shared by reference rather than duplicated. Variable nodes are pointer-unique: one heap allocation per variable, so every reference to x is literally the same pointer. Applications, abstractions, and other compound nodes hold references to their children, and every node keeps pointers its type, minimal context, and incoming references. All terms manipulated by a tactic live in the same DAG. Holes (e-vars/metavariables) are also first-class nodes.
The intended workflow: write proofs in MEngine's scripting language (.me files) using built-in tactics (exact, rewrite, induction, match_goal, apply, etc.) or define new tactics directly in the language.
# Install dependencies (if on macOS)
make install-tools
# Build CLI `mengine` and library `libmengine.a`
make
# Run examples
make examplesFor development, it is helpful to generate a .clangd:
make clangdUsage:
./mengine
./mengine path/to/script.me
./mengine --help # for optionsCheck out examples/ for scripts showing the syntax.
This is a prototype! My goals include:
- examples of verifying large imperative programs
- all proofs continue to generate Coq-checkable proof terms
- a tactic scripting language for writing new tactics