|
- Synopsis
-
The Refute Pi Translation Tool automatically
enumerates translations from the pi-calculus
to the CH-calculus and tries to invalidate them
from being convergence equivalent.
The tool reports on which translation are rejected
and which not. The non-rejected translations then
may be candidates for correct translations.
The following technical report uses the tool and the background behind the tool development:
Manfred
Schmidt-Schauß and
David
Sabel.
Embedding the pi-calculus into a concurrent functional programming
language.
Frank
report 60, Institut für Informatik. Fachbereich Informatik und
Mathematik. J. W. Goethe-Universität Frankfurt am Main, May 2020.
[ PDF]
The tool is implemented in Haskell and packaged via Cabal and comes with
a 3-clause BSD-like LICENSE.
- Download and Building
-
-
The source-distribution is available here:
refute-pi-translations-0.1.0.0.tar.gz
- A recent installation of the Glasgow Haskell Compiler, the base libraries, and Cabal-Install is required (see https://www.haskell.org/downloads)
-
To build the tool, unzip the archive, then run cabal, i.e.:
tar -xzf refute-pi-translations-0.1.0.0.tar.gz
cd refute-pi-translations-0.1.0.0/
cabal configure
cabal build
This will create the executable refute-pi-translations in dist/build/refute-pi-translations , e.g. type
dist/build/refute-pi-translations/refute-pi-translations
to execute the tool.
- Generated Output
The output generated by our tool for several kinds of translations
is collected here (large output files are gzip-compressed):
Simple Translation
Translations with interprocess communication restriction
Translations without interprocess communication restriction
- Contact
-
Dr. David Sabel
|