Minuska - a formally verified semantic framework

Minuska is a framework for defining operational semantics ("language definitions") of programming languages and deriving tools from them. Currently, the project is a research prototype, and the only tools derivable from language definitions are interpreters. Users looking for a mature programming language framework are advised to check out K framework or PLT-Redex. (For a more detailed comparison to K framework, look here.)

Minuska is built on top of the Coq proof assistant. At its core is a simple language MinusLang for expressing programming language semantics in an exact, unambiguous way: MinusLang has a simple formal semantics (mechanized in spec.v), and every MinusLang definition induces a transition relation between program configurations. Similarly, in Minuska we can mathematically describe what a particular tool for a given language should do. For example, a step interpreter takes a program configuration and either returns a next configuration, or returns None. We have defined what does it mean for an interpreter to be correct with respect to a language definition, defined some mild criteria for when a language definition is amenable to interpretation, created a very simple generic interpreter that is parametric in a MinusLang language definition, and proved it correct.

There are two ways of writing a language definition in Minuska: either as a Coq definition (example), or as a standalone *.m file (example) that can be automatically converted to a Coq *.v file:

minuska def2coq language.m language.v

As for the generated interpreters: these can also be used either from inside the Coq, or compiled (using Coq's extraction mechanism) into a standalone executable file:

minuska compile language.m language-interpreter.exe

Note that the minuska command is still under an active development: it is not feature complete and may contain bugs. More importantly, the command-line interface is NOT formally verified, as it is written in OCaml rather than Coq.

Using Minuska

The simplest way is to use the provided Nix Flake

nix develop '.#with-minuska'

which provides the minuska command, as well as the required version of Coq and its libraries. Consult the user guide for more details.

Working on Minuska

The easiest way to start is using the Nix Flake:

nix develop '.#minuska'
cd minuska/

See the developer guide for more details. Also, see CoqDoc

Missing features

In principle, many features could be implemented in Minuska that would make the framework more useful. These include support for concrete syntax of programming languages, formalization of the strictness declarations, symbolic execution, and deductive verification. See the ideas document

Troubleshooting

If your system does not support FUSE, or its configuration is broken, try export APPIMAGE_EXTRACT_AND_RUN=1 before running any generated interpreters. This needs to be done e.g., in Docker, or when running on Github-hosted runners.

Papers

An extended version of the preliminary 'Minuska: Towards a Formally Verified Programming Language Framework' paper is available here.