SUBSEXPL

SUBSEXPL (acronymous for SUBStituições EXPLícitas) is an OCAML implementation of reduction via the explicit substitutions calculi. The current implementation allows reductions in the lambda calculus with names and in the following calculi of explicit substitutions: The reductions can be easily recorded and stored into files; latex output is also provided. Now there exists a version of SUBSEXPL which includes a new graphical interface over emacs with the x-symbol mode that provides a much better user interface. With this interface lambda-expressions are visualized directly, without the necessity to produce the latex output as before.

Reference

  • A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi. F. L. C. de Moura, A. V. Barbosa, M. Ayala-Rincón, F. Kamareddine. 5th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2010), 2011. [MBAK11]

    Downloads

    New extension: SUBSEXPL 2.0

  • Click here to download the source code (GNU/linux x86).

    Binaries

  • Click here to download just the binary file for PC like machines (GNU/linux x86).
  • Click here to download just the binary file for macintosh machines (PowerPC).
  • Click here text file that contains alias for lambda terms.

    To run this binary file, first creat an empty file called "alias.txt", i.e., type "touch alias.txt", then download the binary "subsexpl???.bin" (??? can be equal to 'x86' for PC machines or 'ppc' if you have a MAC (PowerPC machine) and the file "alias_common.txt". Turn the file by typing "chmod +x subsexpl???.bin". Then, start emacs and then type "M-x shell" to start a shell within an emacs window. Assuming that you have x-symbol already installed, start x-symbol mode by typing "M-x x-symbol-mode". Then emacs will ask you about the "Token Language for X-Symbol mode:" and you should type "TeX macro" and then ENTER. To start SUBSEXPL type "./subsxsymb???.bin" in this emacs shell.

    Full source code (plataform independent)

  • Click here to download the full source code including examples and installation instructions.

    To expand this file type "tar zxpvf subsxsymbol.tar.gz" in a terminal. It will create the directory "subsexpl-x-symbol" that contains the file README containing all installation details.

    Last modification: 27/05/2010.