From Program Logics to Language Logics

TL;DR

The paper introduces language logics as a Hoare-style counterpart for language verification, enabling statements of the form $\{P\}\ \mathcal{X}\ \{Q\}$ where $\mathcal{X}$ denotes a language component. It defines $\mathbb{L}$, a concrete language logic with inductive, ctx-compliant, contravariant, and other predicates, plus a set of proof rules for traversing grammars and inference rules. An automated prover, Lang-n-Assert, demonstrates the approach on a faulty language $\lambda^{\div}_{\mathtt{print}}$, reproducing debugging steps and validating fixes, though the authors acknowledge that language verification remains out of reach due to missing soundness guarantees. Despite these limitations, the work provides a concrete framework for applying program-logics-style reasoning to language definitions and lays groundwork for future formalization and broader analyses of language design aspects.

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.

Figures (3)

• Figure 1: Language definition of $\lambda^{\div}_{\mathtt{print}}$
• Figure 2: Main proof rules of $\mathbb{L}$. We have $\mathcal{X}\in\{\mathcal{L}, G, I, g, r\}$.
• Figure 3: Proof rules for $\{P\}~g~\{Q\}$ and $\{P\}~r~\{Q\}$. Notation $\,\widetilde{\cdot}\,$ denotes finite sequences.