Minuska: Towards a Formally Verified Programming Language Framework

TUŠIL, Jan a 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 s.

Základní údaje

Originální název

Minuska: Towards a Formally Verified Programming Language Framework

Název česky

Minuska: Směrem k Formálně Verifikovanému Frameworku pro Programovací Jazyky

Autoři

TUŠIL, Jan a Jan OBDRŽÁLEK

Vydání

Aveiro, Portugal, 22nd International Conference on Software Engineering and Formal Methods, 15 s. 2024

Nakladatel

Springer Nature Switzerland AG

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

programming language semantics; interpreter; semantic framework; Coq

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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.