From 076251bd8ecd40804b8e3d7790f62f7b8152b212 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 28 Dec 2023 16:39:05 +0300 Subject: [PATCH] Update README --- README.md | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index e79aa0c3..41c18816 100644 --- a/README.md +++ b/README.md @@ -1,14 +1,28 @@ -# Proof of 𝜑-calculus confluence. - -Formalization of 𝜑-calculus. +# Confluence for 𝜑-calculus +Formalization of 𝜑-calculus variants and corresponding confluence results. ## About -We aim to formalize 𝜑-calculus and its properties in Lean 4. We first focus on proving confluence of minimal version of a calculus, and then we plan to add features and obtain a proof for the extended version. +We aim to formalize, using a computer proof assistant Lean 4, +𝜑-calculus and the rewrite rules for normalization +of 𝜑-programs (see ). +We are particularly interested in the confluence of the rewrite system. +To formalize this, we first focus on the minimal version of the calculus[^1], +and then gradually add features to match [EO](https://github.com/objectionary/eo)[^2]. ## Installation -To install Lean4, install [`elan`](https://github.com/leanprover/elan), version manager for Lean. +If you use VS Code, get [lean4 extension](https://github.com/leanprover/vscode-lean4). +Otherwise, install [`elan`](https://github.com/leanprover/elan), version manager for Lean. + +In VScode, make sure to open the root directory of the project. +Then run the following from the Terminal: + +```sh +lake build +``` + +[^1]: 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. -If you use VScode, get [lean4 extension](https://github.com/leanprover/vscode-lean4). In VScode, make sure to open root folder of the project. Then run `lake build`. \ No newline at end of file +[^2]: Yegor Bugayenko. 2022. _EOLANG and φ-calculus._