Minuska: Towards a Formally Verified Programming Language Framework
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F25%3A00140287" target="_blank" >RIV/00216224:14330/25:00140287 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1007/978-3-031-77382-2_12" target="_blank" >http://dx.doi.org/10.1007/978-3-031-77382-2_12</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-77382-2_12" target="_blank" >10.1007/978-3-031-77382-2_12</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Minuska: Towards a Formally Verified Programming Language Framework
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Minuska: Towards a Formally Verified Programming Language Framework
Popis výsledku anglicky
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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
—
Návaznosti
S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2025
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
22nd International Conference on Software Engineering and Formal Methods, SEFM 2024
ISBN
9783031773815
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
15
Strana od-do
200-214
Název nakladatele
Springer Nature Switzerland AG
Místo vydání
Aveiro, Portugal
Místo konání akce
Aveiro, Portugal
Datum konání akce
1. 1. 2024
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
001538050700012