From Program Logics to Language Logics
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866913457530470400 |
|---|---|
| author | Cimini, Matteo |
| author_facet | Cimini, Matteo |
| contents | Program logics are a powerful formal method in the context of program verification. Can we develop a counterpart of program logics in the context of language verification? This paper proposes language logics, which allow for statements of the form $\{P\}\ \mathcal{X}\ \{Q\}$ where $\mathcal{X}$, the subject of analysis, can be a language component such as a piece of grammar, a typing rule, a reduction rule or other parts of a language definition. To demonstrate our approach, we develop $\mathbb{L}$, a language logic that can be used to analyze language definitions on various aspects of language design. We illustrate $\mathbb{L}$ to the analysis of some selected aspects of a programming language. We have also implemented an automated prover for $\mathbb{L}$, and we confirm that the tool repeats these analyses. Ultimately, $\mathbb{L}$ cannot verify languages. Nonetheless, we believe that this paper provides a strong first step towards adopting the methods of program logics for the analysis of languages. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_01515 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | From Program Logics to Language Logics Cimini, Matteo Programming Languages Program logics are a powerful formal method in the context of program verification. Can we develop a counterpart of program logics in the context of language verification? This paper proposes language logics, which allow for statements of the form $\{P\}\ \mathcal{X}\ \{Q\}$ where $\mathcal{X}$, the subject of analysis, can be a language component such as a piece of grammar, a typing rule, a reduction rule or other parts of a language definition. To demonstrate our approach, we develop $\mathbb{L}$, a language logic that can be used to analyze language definitions on various aspects of language design. We illustrate $\mathbb{L}$ to the analysis of some selected aspects of a programming language. We have also implemented an automated prover for $\mathbb{L}$, and we confirm that the tool repeats these analyses. Ultimately, $\mathbb{L}$ cannot verify languages. Nonetheless, we believe that this paper provides a strong first step towards adopting the methods of program logics for the analysis of languages. |
| title | From Program Logics to Language Logics |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2408.01515 |