Papers › Mechanization of LAGC Semantics in Isabelle
Mechanization of LAGC Semantics in Isabelle
Niklas Heidler
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
Formal programming language semantics are imperative when trying to verify properties of programs in an automated manner. Using a new approach, Din et al. strengthen the ability of reasoning about concurrent programs by proposing a modular trace semantics, which can flexibly adapt to the most prominent imperative programming language paradigms. These semantics decouple the evaluation in the local environments from the evaluation in the global environment by generating abstract, symbolic traces for the individual, local systems. The traces are then composed and concretized, resulting in global traces for the global system. Hence, these semantics are called Locally Abstract, Globally Concrete (LAGC). In this work, we present a formalization of the LAGC semantics in the popular theorem proving environment Isabelle/HOL. The given model is based on the prior work on the theory of LAGC semantics by Din et al. and includes formalizations of the basic theorems, the LAGC semantics for the While Language (WL), as well as the LAGC semantics for an extended version of the While Language (WLEXT). We furthermore use our Isabelle model in order to provide formal proofs for several advanced properties of the LAGC semantics, which have not been analyzed in the original paper. Whilst the main goal of the work was to formalize the LAGC semantics in a mathematically rigorous manner, we also achieve a high level of proof automatization and manage to contribute an efficient code-generation for the computation of program traces. As the formalization of the semantics is highly modular, the given theories could in the future be extended with even more sophisticated programming language paradigms.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections