arXiv subjects

Péter Bereczky

Publications and source records attributed to Péter Bereczky.

9 recordsLinked to original sources

arXiv2026

Dependently Typed Model Composition for Matching Logic

This paper investigates model compositionâ€”often referred to as "gluing"â€”within the framework of matching logic. Specifically, we examine the systematic combination of existing signatures, variable valuations, theories, and their corresponding models. Our primary objective is to ensure that this composition preserves satisfaction proofs; that is, any theory validated by the individual constituent models is also validated by the resulting composite model. Our definitions are based on a polyadic, sorted variant of matching logic, which has also been expressed in the Rocq proof assistant. Therefore, we outline our definitions with dependent types for this work to serve as a direct blueprint for the mechanization in the short-term future.

cs.LO↗

arXiv2025

On a Dependently Typed Encoding of Matching Logic

Matching logic is a general formal framework for reasoning about a wide range of theories, with particular emphasis on programming language semantics. Notably, the intermediate language of the K semantics framework is an extension of matching $μ$-logic, a sorted, polyadic variant of the logic. Metatheoretic reasoning requires the logic to be expressed within a foundational theory; opting for a dependently typed one enables well-sortedness in the object theory to correspond directly to well-typedness in the host theory. In this paper, we present the first dependently typed definition of matching $μ$-logic, ensuring well-sortedness via sorted contexts encoded in type indices. As a result, ill-sorted syntax elements are unrepresentable, and the semantics of well-sorted elements are guaranteed to lie within the domain of their associated sort.

cs.LO↗

arXiv2024

Unification in Matching Logic -- Revisited

Matching logic is a logical framework for specifying and reasoning about programs using pattern matching semantics. A pattern is made up of a number of structural components and constraints. Structural components are syntactically matched, while constraints need to be satisfied. Having multiple structural patterns poses a practical problem as it requires multiple matching operations. This is easily remedied by unification, for which an algorithm has already been defined and proven correct in a sorted, polyadic variant of matching logic. This paper revisits the subject in the applicative variant of the language while generalising the unification problem and mechanizing a proven-sound solution in Coq.

cs.LO↗

arXiv2023

A Formalisation of Core Erlang, a Concurrent Actor Language

In order to reason about the behaviour of programs described in a programming language, a mathematically rigorous definition of that language is needed. In this paper, we present a machine-checked formalisation of concurrent Core Erlang (a subset of Erlang) based on our previous formalisations of its sequential sublanguage. We define a modular, frame stack semantics, show how program evaluation is carried out with it, and prove a number of properties (e.g. determinism, confluence). Finally, we define program equivalence based on bisimulations and prove that side-effect-free evaluation is a bisimulation. This research is part of a wider project that aims to verify refactorings to prove that particular program code transformations preserve program behaviour.

cs.PL↗

arXiv2023

A Frame Stack Semantics for Sequential Core Erlang

We present a small-step, frame stack style, semantics for sequential Core Erlang, a dynamically typed, impure functional programming language. The semantics and the properties that we prove are machine-checked with the Coq proof assistant. We improve on previous work by including exceptions and exception handling, as well as built-in data types and functions. Based on the semantics, we define multiple concepts of program equivalence (contextual, CIU equivalence, and equivalence based on logical relations) and prove that the definitions are all equivalent. Using this we are able to give a correctness criterion for refactorings by means of contextually equivalent symbolic expression pairs, which is one of the main motivations of this work.

cs.PL↗

arXiv2022

Mechanizing Matching Logic In Coq

Matching logic is a formalism for specifying, and reasoning about, mathematical structures, using patterns and pattern matching. Growing in popularity, it has been used to define many logical systems such as separation logic with recursive definitions and linear temporal logic. In addition, it serves as the logical foundation of the K semantic framework, which was used to build practical verifiers for a number of real-world languages. Despite being a fundamental formal system accommodating substantial theories, matching logic lacks a general-purpose, machine-checked formalization. Hence, we formalize matching logic using the Coq proof assistant. Specifically, we create a new representation of matching logic that uses a locally nameless encoding, and we formalize the syntax, semantics, and proof system of this representation in the Coq proof assistant. Crucially, we prove the soundness of the formalized proof system and provide a means to carry out interactive matching logic reasoning in Coq. We believe this work provides a previously unexplored avenue for reasoning about matching logic, its models, and the proof system.

cs.LO↗

arXiv2022

Program Equivalence in an Untyped, Call-by-value Lambda Calculus with Uncurried Recursive Functions

We aim to reason about the correctness of behaviour-preserving transformations of Erlang programs. Behaviour preservation is characterised by semantic equivalence. Based upon our existing formal semantics for Core Erlang, we investigate potential definitions of suitable equivalence relations. In particular we adapt a number of existing approaches of expression equivalence to a simple functional programming language that carries the main features of sequential Core Erlang; we then examine the properties of the equivalence relations and formally establish connections between them. The results presented in this paper, including all theorems and their proofs, have been machine checked using the Coq proof assistant.

cs.PL↗

arXiv2020

A Comparison of Big-step Semantics Definition Styles

Formal semantics provides rigorous, mathematically precise definitions of programming languages, with which we can argue about program behaviour and program equivalence by formal means; in particular, we can describe and verify our arguments with a proof assistant. There are various approaches to giving formal semantics to programming languages, at different abstraction levels and applying different mathematical machinery: the reason for using the semantics determines which approach to choose. In this paper we investigate some of the approaches that share their roots with traditional relational big-step semantics, such as (a) functional big-step semantics (or, equivalently, a definitional interpreter), (b) pretty-big-step semantics and (c) traditional natural semantics. We compare these approaches with respect to the following criteria: executability of the semantics definition, proof complexity for typical properties (e.g. determinism) and the conciseness of expression equivalence proofs in that approach. We also briefly discuss the complexity of these definitions and the coinductive big-step semantics, which enables reasoning about divergence. To enable the comparison in practice, we present an example language for comparing the semantics: a sequential subset of Core Erlang, a functional programming language, which is used in the intermediate steps of the Erlang/OTP compiler. We have already defined a relational big-step semantics for this language that includes treatment of exceptions and side effects. The aim of this current work is to compare our big-step definition for this language with a variety of other equivalent semantics in different styles from the point of view of testing and verifying code refactorings.

cs.PL↗

arXiv2020

A Proof Assistant Based Formalisation of Core Erlang

Our research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations of Erlang programs. In order to formally reason about the definition of a programming language and the software built using it, we need a mathematically rigorous description of that language. In this paper, we present our proof-assistant-based formalisation of a subset of Erlang, intended to serve as a base for proving refactorings correct. After discussing how we reused concepts from related work, we show the syntax and semantics of our formal description, including the abstractions involved (e.g. closures). We also present essential properties of the formalisation (e.g. determinism) along with their machine-checked proofs. Finally, we prove the correctness of some simple refactoring strategies.

cs.PL↗