Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{2428109,
author = {Tušil, Jan and Obdržálek, Jan},
address = {Aveiro, Portugal},
booktitle = {22nd International Conference on Software Engineering and Formal Methods},
editor = {Alexandre Madeira and Alexander Knapp},
keywords = {programming language semantics; interpreter; semantic framework; Coq},
howpublished = {elektronická verze "online"},
language = {eng},
location = {Aveiro, Portugal},
publisher = {Springer Nature Switzerland AG},
title = {Minuska: Towards a Formally Verified Programming Language Framework},
year = {2024}
}
TY - JOUR
ID - 2428109
AU - Tušil, Jan - Obdržálek, Jan
PY - 2024
TI - Minuska: Towards a Formally Verified Programming Language Framework
PB - Springer Nature Switzerland AG
CY - Aveiro, Portugal
KW - programming language semantics
KW - interpreter
KW - semantic framework
KW - Coq
N2 - 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.
ER -
TUŠIL, Jan a Jan OBDRŽÁLEK. Minuska: Towards a Formally Verified Programming Language Framework. Online. In Alexandre Madeira and Alexander Knapp. \textit{22nd International Conference on Software Engineering and Formal Methods}. Aveiro, Portugal: Springer Nature Switzerland AG, 2024, 15 s.
|
