Publication details
Minuska: Towards a Formally Verified Programming Language Framework
| Authors | |
|---|---|
| Year of publication | 2024 |
| Type | Article in Proceedings |
| Conference | 22nd International Conference on Software Engineering and Formal Methods |
| MU Faculty or unit | |
| Citation | TUŠIL, Jan and Jan OBDRŽÁLEK. Minuska: Towards a Formally Verified Programming Language Framework. Online. In Alexandre Madeira and Alexander Knapp. 22nd International Conference on Software Engineering and Formal Methods. Aveiro, Portugal: Springer Nature Switzerland AG, 2024, 15 pp. |
| Keywords | programming language semantics; interpreter; semantic framework; Coq |
| Description | 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 non-trivial languages while performing well. |
| Related projects: |