# 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:
- lambda-sigma calculus [ACCL91]
- lambda s
_{e}-calculus [KR97]
- the suspension calculus [NAD99]
- a refinement of the suspension calculus which
combines steps of beta-contraction. [NQ03]

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.