Formalization of 𝜑-calculus variants and corresponding confluence results.
We aim to formalize, using a computer proof assistant Lean 4, 𝜑-calculus and the rewrite rules for normalization of 𝜑-programs (see https://github.com/objectionary/normalizer). We are particularly interested in the confluence of the rewrite system. To formalize this, we first focus on the minimal version of the calculus1, and then gradually add features to match EO2.
If you use VS Code, get lean4 extension.
Otherwise, install elan, version manager for Lean.
In VScode, make sure to open the root directory of the project. Then run the following from the Terminal:
lake buildFootnotes
-
Nikolai Kudasov and Violetta Sim. 2023. Formalizing 𝜑-Calculus: A Purely Object-Oriented Calculus of Decorated Objects. In Proceedings of the 24th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP '22). Association for Computing Machinery, New York, NY, USA, 29–36. https://doi.org/10.1145/3611096.3611103 ↩
-
Yegor Bugayenko. 2022. EOLANG and φ-calculus. https://arxiv.org/abs/2111.13384 ↩