Minuska: Towards a Formally Verified Programming Language Framework

TL;DR

A practical formal programming language framework called Minuska is introduced, which always generates a provably correct interpreter given a valid language definition and uses the Coq proof assistant to implement an interpreter parametric in a MinusLang definition and to prove it correct.

Abstract

Programming language frameworks allow us to generate language tools (e.g., interpreters) just from a formal description of the syntax and semantics of a programming language. As these frameworks tend to be quite complex, an issue arises whether we can trust the generated tools. To address this issue, we introduce a practical formal programming language framework called Minuska, which always generates a provably correct interpreter given a valid language definition. This is achieved by (1) defining a language MinusLang for expressing programming language definitions and giving it formal semantics and (2) using the Coq proof assistant to implement an interpreter parametric in a MinusLang definition and to prove it correct. Minuska provides strong correctness guarantees and can support nontrivial languages while performing well. This is the extended version of the SEFM24 paper of the same name.

Figures (6)

• Figure 1: A fragment of the formal semantics of a simple imperative language, written in the sugared concrete syntax of Minuska.
• Figure 2: "two-counters": the running example of ChenLTR20 in Minuska. "Native compute time" means wall-clock time of the system executed in an extracted and compiled standalone interpreter. "Compute time" is the time needed to evaluate the benchmark using Coq's Compute command, and "coqc time" is time needed to evaluate a Coq (*.v) file containing the command.
• Figure 3: Running times of shared $\mathbb{K}$/Minuska benchmarks. The meaning of the columns is as follows. For $\mathbb{K}$, "$\mathbb{K}$ parameters" is the time required to generate proof parameters for a single execution, including time required argument parsing; "$\mathbb{K}$ cert-gen" is the time of certificate generation from those parameters; and "$\mathbb{K}$ cert-check" is the time required for checking those certificates. For Minuska, "M compute" is the time to evaluate the benchmark using Coq's Compute mechanism, measured inside Coq using its Time command; and "M coqc" is the the time required for Coq to process a file with the benchmark, as measured by the GNU time utility.
• Figure 4: Running times of a program for computing $\Sigma_{i=i}^{n} i$ in a simple imperative language IMP with semantics defined in Minuska. 'Compute' means the time of the 'Compute' command within Coq, 'coqc' means the total time of the 'coqc' command on a file containing the Compute command, and 'native' means the time of the native code generated by the OCaml compiler for the interpreter extracted from Coq into OCaml.
• Figure 5: Other benchmarks of Minuska

Theorems & Definitions (8)

• Theorem 1
• Lemma 1: tryMatch correct
• proof
• Lemma 2: evaluateCondition
• proof
• Lemma 3: evaluate correct
• proof
• proof