Sciweavers

ENTCS
2011

A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi

12 years 9 months ago
A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi
SUBSEXPL is a system originally developed to visualise reductions, simplifications and normalisations in three important calculi of explicit substitutions and has been applied to understand and explain properties of these calculi and to compare the different styles of making explicit the substitution operation in implementations of the λ-calculus in de Bruijn notation. The system was developed in OCaml and now it can be executed inside the Emacs editor within a new mode which allows a very easy interaction. The use of special symbols makes its application very useful for students because the notation on the screen is as close as possible to that on the papers. In addition to λ-calculus and explicit substitutions calculi in de Bruijn notation, now it is possible to work with the λ-calculus with variables as names and with several calculi of explicit substitutions using also representation of variables with names. Moreover, in contrast to the original version of the system, that wa...
F. L. C. de Moura, A. V. Barbosa, Mauricio Ayala-R
Added 14 May 2011
Updated 14 May 2011
Type Journal
Year 2011
Where ENTCS
Authors F. L. C. de Moura, A. V. Barbosa, Mauricio Ayala-Rincón, Fairouz Kamareddine
Comments (0)