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

TL;DR

This paper explores semantic equivalence in an untyped, call-by-value lambda calculus with uncurried recursive functions, aiming to verify program transformations in Erlang through formal semantics and machine-checked proofs.

Contribution

It adapts and analyzes various expression equivalence approaches for a Core Erlang-like language, establishing formal properties and connections between them using Coq.

Findings

Formal semantics for Core Erlang are developed.

Multiple equivalence relations are adapted and compared.

All theorems and proofs are machine-verified in Coq.

Abstract

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.