activity
20202026
most citedMechanizing Matching Logic In Coq

7 citations · 12 across the 9 of their papers we have counts for

collaborators
Showing cs.PLShow all

5 papers · 1 filter

cs.PL2023

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…

cs.PL2023

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…

cs.PL2022

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…

cs.PL2020★ 1 cited

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…

cs.PL2020★ 4 cited

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…