2024/08/02 by Matteo Cimini, Cimini, Matteo
Computer Science · #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Advanced Algebra and Logic
paper · pdf · doi:10.48550/arxiv.2408.01515
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\ X \Q\ where 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 \mathbbL, a language logic that can be used to analyze language definitions on various aspects of language design. We illustrate \mathbbL to the analysis of some selected aspects of a programming language. We have also implemented an automated prover for \mathbbL, and we confirm that the tool repeats these analyses. Ultimately, \mathbbL 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.