The Refute Pi Translations Tool


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
(c) 2020 David Sabel, Imprint, Privacy Policy Last modified: $Author: sabel $, $Date: 2020/05/16 10:28:03 $