7 citations · 12 across the 9 of their papers we have counts for
9 papers
Dependently Typed Model Composition for Matching Logic
Ádám Kurucz, Péter Bereczky, Dániel Horpácsi
This paper investigates model composition—often referred to as "gluing"—within the framework of matching logic. Specifically, we examine the systematic combination of existing…
On a Dependently Typed Encoding of Matching Logic
Ádám Kurucz, Péter Bereczky, Dániel Horpácsi
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 lan…
Unification in Matching Logic -- Revisited
Ádám Kurucz, Péter Bereczky, Dániel Horpácsi
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 co…
A Formalisation of Core Erlang, a Concurrent Actor Language
Péter Bereczky, Dániel Horpácsi, Simon Thompson
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…
A Frame Stack Semantics for Sequential Core Erlang
Péter Bereczky, Dániel Horpácsi, Simon Thompson
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…
Program Equivalence in an Untyped, Call-by-value Lambda Calculus with Uncurried Recursive Functions
Dániel Horpácsi, Péter Bereczky, Simon Thompson
We aim to reason about the correctness of behaviour-preserving transformations of Erlang programs. Behaviour preservation is characterised by semantic equivalence. Based upon our e…
Mechanizing Matching Logic In Coq
Péter Bereczky, Xiaohong Chen, Dániel Horpácsi +2
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 m…
A Comparison of Big-step Semantics Definition Styles
Péter Bereczky, Dániel Horpácsi, Simon Thompson
Formal semantics provides rigorous, mathematically precise definitions of programming languages, with which we can argue about program behaviour and program equivalence by formal m…
A Proof Assistant Based Formalisation of Core Erlang
Péter Bereczky, Dániel Horpácsi, Simon Thompson
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 formal…