On November 20, 2025, at 14:00 EET, Horaศiu Cheval (University of Bucharest) will give a talk in the Logic Seminar.
Title: ๐ definitions as Matching Logic theories
Abstract:
The ๐ Framework is a rewriting-based tool for specifying programming language semantics and carrying out formal verification based on the semantics given.
PL definitions are translated by ๐ into Matching Logic (ML) theories, encoded in an intermediate language named Kore, through a complex compilation process which is not formally documented and has to be considered as part of the trusted codebase.
In this talk, we describe a formal mechanism for obtaining the denotational semantics of ๐ definitions directly as ML theories.
While for many components of ๐, the ML denotation we give is similar to the current Kore output, abstract rewrite rules, which allow one to specify rewrite rules by mentioning only the fragments of the program configuration that are being modified and are one of ๐โs most important features, lack at the moment an elegant ML denotation.
In the current implementation of ๐, they are compiled through a mechanism of configuration concretization which converts them into top rewrite rules between full configurations. Based on a newly developed ML theory of contexts, we propose a solution through which we can uniformly axiomatize such abstract rules in a way that reflects their local nature and does not rely on a concretization algorithm.
This is joint work with Xiaohong Chen, Dorel Lucanu and Grigore Roศu.
The talk will take place physically at FMI (the new PBTower location), Hall 203.