تقرير
Program Equivalence in an Untyped, Call-by-value Lambda Calculus with Uncurried Recursive Functions
| العنوان: | Program Equivalence in an Untyped, Call-by-value Lambda Calculus with Uncurried Recursive Functions |
|---|---|
| المؤلفون: | Horpácsi, Dániel, Bereczky, Péter, Thompson, Simon |
| سنة النشر: | 2022 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Programming Languages |
| الوصف: | 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. Comment: Submitted to the Journal of Logical and Algebraic Methods in Programming |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2208.14260 |
| رقم الأكسشن: | edsarx.2208.14260 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |