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...

• Type: Journal
• Year: 2011
• Where: ENTCS
• Authors: F. L. C. de Moura, A. V. Barbosa, Mauricio Ayala-Rincón, Fairouz Kamareddine
• Keywords: Bruijn Notation, ENTCS 2011, Explicit Substitutions, Important Calculi