A Formalization of the Reversible Concurrent Calculus CCSKP in Beluga (artifact)
Fuente:
Zenodo
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Recurso digital |
| Veröffentlicht: |
Zenodo
2025
|
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866901966245855232 |
|---|---|
| author | Cecilia, Gabriele |
| author_facet | Cecilia, Gabriele |
| contents | <h1><strong>Overview</strong></h1> <p>This artifact contains the source code for the paper "A Formalization of the Reversible Concurrent Calculus CCSK^P in Beluga" (<a href="https://ice-workshop.github.io/">ICE 2025</a>).</p> <p>The <code>code\</code> repository provides an overview of the files and a paper-to-artifact table. Below are install and usage instructions.</p> <h2><strong>Install instructions</strong></h2> <p>This mechanization is compatible with <a href="https://complogic.cs.mcgill.ca/beluga/">Beluga</a> version 1.1.1.</p> <p>For installation, please refer to the <a href="https://github.com/Beluga-lang/Beluga/blob/master/INSTALL">installation guide</a> in the GitHub repository of Beluga. Below is a summary.</p> <h3><strong>Prerequisites</strong></h3> <p>The following must be installed before proceeding with the installation of Beluga:</p> <p>- opam 2.1.4+: <a href="https://opam.ocaml.org/doc/Install.html">https://opam.ocaml.org/doc/Install.html</a><br>- GNU Make 4.0+: <a href="https://www.gnu.org/software/make/">https://www.gnu.org/software/make/</a><br>- (optional, for improved beli mode) rlwrap: <a href="https://github.com/hanslub42/rlwrap">https://github.com/hanslub42/rlwrap</a></p> <h3><strong>Debian/Ubuntu</strong></h3> <p>All the necessary prerequisites can be installed with the following commands:</p> <blockquote> <p>apt-get install opam<br>opam init --bare</p> </blockquote> <p>Once opam is installed, it is possible to directly run the following command:</p> <blockquote> <p>opam install beluga</p> </blockquote> <p>Alternatively, it is possible to run these commands from the Beluga directory, available in the <a href="https://github.com/Beluga-lang/Beluga/blob/master/INSTALL">installation guide</a> in the GitHub repository of Beluga:</p> <blockquote> <p>make setup-install<br>make install</p> </blockquote> <h3><strong>macOS</strong></h3> <p>The easiest way to install the prerequisites is via opam, and the easiest way to install opam is via Homebrew (<a href="https://brew.sh/">https://brew.sh/</a>):</p> <blockquote> <p>brew install opam<br>opam init --bare</p> </blockquote> <p>Once opam is installed, it is possible to directly run the following command:</p> <blockquote> <p>opam install beluga</p> </blockquote> <p>Alternatively, it is possible to run these commands from the Beluga directory, available in the <a href="https://github.com/Beluga-lang/Beluga/blob/master/INSTALL">installation guide</a> in the GitHub repository of Beluga:</p> <blockquote> <p>make setup-install<br>make install</p> </blockquote> <h3><strong>Windows</strong></h3> <p>One option is to install the Ubuntu WSL distribution (<a href="https://docs.microsoft.com/en-us/windows/wsl/install">https://docs.microsoft.com/en-us/windows/wsl/install</a>) and follow the instructions for Debian/Ubuntu systems.</p> <p>Another option is to build and execute Beluga on Windows through Cygwin. The necessary prerequisites can be installed using opam for Windows. Here are the steps to follow for the installation through Cygwin:</p> <p>1. Download opam for Windows' graphical installer OCaml32/64.exe <a href="https://fdopen.github.io/opam-repository-mingw/installation/">https://fdopen.github.io/opam-repository-mingw/installation/</a></p> <p>2. Run OCaml32/64.exe and step through the installation wizard. Note: if you don't already have Cygwin installed, it will be installed for you.</p> <p>3. Run the following commands from Beluga directory within cygwin terminal.</p> <blockquote> <p>opam switch create ocaml-variants.4.09.0+mingw64c<br>eval $(opam env)</p> </blockquote> <p><br>And then, from the Beluga directory:</p> <blockquote> <p>opam install --deps-only ./beluga.opam</p> </blockquote> <h2><strong>Usage instructions</strong></h2> <p>Once Beluga is installed, it is possible to run Beluga programs with the newly built "beluga" executable. Before, it might be necessary to execute the command <code>eval $(opam env)</code> to enable the correct opam switch.</p> <p>To type-check this artifact, you can run the "beluga" executable on the file <code>all.cfg</code>. The following is the expected output:</p> <blockquote> <p>>> beluga all.cfg<br>## Type Reconstruction begin: code/1_definitions.bel ##<br>## Type Reconstruction done: code/1_definitions.bel ##<br>## Type Reconstruction begin: code/2_basic_properties.bel ##<br>## Type Reconstruction done: code/2_basic_properties.bel ##<br>## Type Reconstruction begin: code/3_lemmas_connectivity_relationship_one.bel ##<br>## Type Reconstruction done: code/3_lemmas_connectivity_relationship_one.bel ##<br>## Type Reconstruction begin: code/4_connectivity_relationship_one.bel ##<br>## Type Reconstruction done: code/4_connectivity_relationship_one.bel ##<br>## Type Reconstruction begin: code/5_lemmas_connectivity_relationship_two.bel ##<br>## Type Reconstruction done: code/5_lemmas_connectivity_relationship_two.bel ##<br>## Type Reconstruction begin: code/6_connectivity_relationship_two.bel ##<br>## Type Reconstruction done: code/6_connectivity_relationship_two.bel ##<br>## Type Reconstruction begin: code/7_complementarity.bel ##<br>## Type Reconstruction done: code/7_complementarity.bel ##</p> </blockquote> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_16179366 |
| institution | Zenodo |
| language | |
| publishDate | 2025 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | A Formalization of the Reversible Concurrent Calculus CCSKP in Beluga (artifact) Cecilia, Gabriele <h1><strong>Overview</strong></h1> <p>This artifact contains the source code for the paper "A Formalization of the Reversible Concurrent Calculus CCSK^P in Beluga" (<a href="https://ice-workshop.github.io/">ICE 2025</a>).</p> <p>The <code>code\</code> repository provides an overview of the files and a paper-to-artifact table. Below are install and usage instructions.</p> <h2><strong>Install instructions</strong></h2> <p>This mechanization is compatible with <a href="https://complogic.cs.mcgill.ca/beluga/">Beluga</a> version 1.1.1.</p> <p>For installation, please refer to the <a href="https://github.com/Beluga-lang/Beluga/blob/master/INSTALL">installation guide</a> in the GitHub repository of Beluga. Below is a summary.</p> <h3><strong>Prerequisites</strong></h3> <p>The following must be installed before proceeding with the installation of Beluga:</p> <p>- opam 2.1.4+: <a href="https://opam.ocaml.org/doc/Install.html">https://opam.ocaml.org/doc/Install.html</a><br>- GNU Make 4.0+: <a href="https://www.gnu.org/software/make/">https://www.gnu.org/software/make/</a><br>- (optional, for improved beli mode) rlwrap: <a href="https://github.com/hanslub42/rlwrap">https://github.com/hanslub42/rlwrap</a></p> <h3><strong>Debian/Ubuntu</strong></h3> <p>All the necessary prerequisites can be installed with the following commands:</p> <blockquote> <p>apt-get install opam<br>opam init --bare</p> </blockquote> <p>Once opam is installed, it is possible to directly run the following command:</p> <blockquote> <p>opam install beluga</p> </blockquote> <p>Alternatively, it is possible to run these commands from the Beluga directory, available in the <a href="https://github.com/Beluga-lang/Beluga/blob/master/INSTALL">installation guide</a> in the GitHub repository of Beluga:</p> <blockquote> <p>make setup-install<br>make install</p> </blockquote> <h3><strong>macOS</strong></h3> <p>The easiest way to install the prerequisites is via opam, and the easiest way to install opam is via Homebrew (<a href="https://brew.sh/">https://brew.sh/</a>):</p> <blockquote> <p>brew install opam<br>opam init --bare</p> </blockquote> <p>Once opam is installed, it is possible to directly run the following command:</p> <blockquote> <p>opam install beluga</p> </blockquote> <p>Alternatively, it is possible to run these commands from the Beluga directory, available in the <a href="https://github.com/Beluga-lang/Beluga/blob/master/INSTALL">installation guide</a> in the GitHub repository of Beluga:</p> <blockquote> <p>make setup-install<br>make install</p> </blockquote> <h3><strong>Windows</strong></h3> <p>One option is to install the Ubuntu WSL distribution (<a href="https://docs.microsoft.com/en-us/windows/wsl/install">https://docs.microsoft.com/en-us/windows/wsl/install</a>) and follow the instructions for Debian/Ubuntu systems.</p> <p>Another option is to build and execute Beluga on Windows through Cygwin. The necessary prerequisites can be installed using opam for Windows. Here are the steps to follow for the installation through Cygwin:</p> <p>1. Download opam for Windows' graphical installer OCaml32/64.exe <a href="https://fdopen.github.io/opam-repository-mingw/installation/">https://fdopen.github.io/opam-repository-mingw/installation/</a></p> <p>2. Run OCaml32/64.exe and step through the installation wizard. Note: if you don't already have Cygwin installed, it will be installed for you.</p> <p>3. Run the following commands from Beluga directory within cygwin terminal.</p> <blockquote> <p>opam switch create ocaml-variants.4.09.0+mingw64c<br>eval $(opam env)</p> </blockquote> <p><br>And then, from the Beluga directory:</p> <blockquote> <p>opam install --deps-only ./beluga.opam</p> </blockquote> <h2><strong>Usage instructions</strong></h2> <p>Once Beluga is installed, it is possible to run Beluga programs with the newly built "beluga" executable. Before, it might be necessary to execute the command <code>eval $(opam env)</code> to enable the correct opam switch.</p> <p>To type-check this artifact, you can run the "beluga" executable on the file <code>all.cfg</code>. The following is the expected output:</p> <blockquote> <p>>> beluga all.cfg<br>## Type Reconstruction begin: code/1_definitions.bel ##<br>## Type Reconstruction done: code/1_definitions.bel ##<br>## Type Reconstruction begin: code/2_basic_properties.bel ##<br>## Type Reconstruction done: code/2_basic_properties.bel ##<br>## Type Reconstruction begin: code/3_lemmas_connectivity_relationship_one.bel ##<br>## Type Reconstruction done: code/3_lemmas_connectivity_relationship_one.bel ##<br>## Type Reconstruction begin: code/4_connectivity_relationship_one.bel ##<br>## Type Reconstruction done: code/4_connectivity_relationship_one.bel ##<br>## Type Reconstruction begin: code/5_lemmas_connectivity_relationship_two.bel ##<br>## Type Reconstruction done: code/5_lemmas_connectivity_relationship_two.bel ##<br>## Type Reconstruction begin: code/6_connectivity_relationship_two.bel ##<br>## Type Reconstruction done: code/6_connectivity_relationship_two.bel ##<br>## Type Reconstruction begin: code/7_complementarity.bel ##<br>## Type Reconstruction done: code/7_complementarity.bel ##</p> </blockquote> |
| title | A Formalization of the Reversible Concurrent Calculus CCSKP in Beluga (artifact) |
| url | https://doi.org/10.5281/zenodo.16179366 |