From Program Logics to Language Logics

TL;DR

This paper introduces language logics, a new formal framework inspired by program logics, to analyze language components such as grammar and rules, demonstrated through the development and implementation of a specific logic called $$, and explores its potential and limitations.

Contribution

The paper develops the concept of language logics, creates a specific logic $$ for language analysis, and implements an automated prover, pioneering a new approach in language verification.

Findings

$$ can analyze various aspects of language design.

Automated prover successfully repeats language analyses.

$$ cannot fully verify languages, indicating limitations.

Abstract

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.