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 following calculi: 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.

Screenshots

screen1 screen2 screen3 screen4

Downloads

version with x-symbol

  • 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 (GNU/linux ppc).

    To run this binary file, turn it into an executable file by typing "chmod +x subsxsymb???.bin" in a terminal replacing ??? by x86 or ppc according to your machine's architecture. 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" that contains the file README containing all installation details.

    version without x-symbol

  • 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 (GNU/linux ppc).

    To run this binary file, turn it into an executable file by typing "chmod +x subsexpl???.bin" in a terminal replacing ??? by x86 or ppc according to your machine's architecture. Then, start emacs and then type "M-x shell" to start a shell within an emacs window. To start SUBSEXPL type "./subsexpl???.bin" in this emacs shell. For more information see the tutorial (pdf) (ps)

    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" that contains the file README containing all installation details.
    Last modification: 04/04/2006.