Minuska: Towards a Formally Verified Programming Language Framework
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Minuska: Towards a Formally Verified Programming Language Framework
Original language 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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
—
Continuities
S - Specificky vyzkum na vysokych skolach
Others
Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
22nd International Conference on Software Engineering and Formal Methods, SEFM 2024
ISBN
9783031773815
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
200-214
Publisher name
Springer Nature Switzerland AG
Place of publication
Aveiro, Portugal
Event location
Aveiro, Portugal
Event date
Jan 1, 2024
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
001538050700012