A flexible framework for visualisation of computational properties of general explicit substitutions calculi. (English) Zbl 1347.68058

Haeusler, Edward Hermann (ed.) et al., Proceedings of the 5th workshop on logical and semantic frameworks, with applications (LSFA 2010), Natal, Brazil, August 31, 2010. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 269, 41-54 (2011).
Summary: 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 \(\lambda\)-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 paper. In addition to dealing the \(\lambda\)-calculus and explicit substitutions calculi in de Bruijn notation, now it is possible to work with the \(\lambda\)-calculus 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 was restricted to three specific calculi of explicit substitution, the new version allows the inclusion of new calculi by giving as input their grammatical descriptions. SUBSEXPL has been used with success for teaching basic properties of the \(\lambda\)-calculus and for illustrating the computational impact of selecting one kind of representation of variables (either names or indices) and a specific style of making explicit substitutions in real implementations based on the \(\lambda\)-calculus.
For the entire collection see [Zbl 1281.68027].


68N18 Functional programming and lambda calculus
68Q42 Grammars and rewriting systems
Full Text: DOI


[1] Abadi, M.; Cardelli, L.; Curien, P.-L.; Lévy, J.-J., Explicit substitutions, Journal of functional programming, 1, 4, 375-416, (1991) · Zbl 0941.68542
[2] Ayala-Rincón, M.; de Moura, F.L.C.; Kamareddine, F., Comparing and implementing calculi of explicit substitutions with eta-reduction, Annals of pure and applied logic, 134, 5-41, (2005) · Zbl 1067.03042
[3] Ayala-Rincón, M.; Muoz, C., Explicit substitutions and all that, Revista colombiana de computación, 1, 1, 47-71, (2000)
[4] Aydemir, B.E.; Charguéraud, A.; Pierce, B.C.; Pollack, R.; Weirich, S., Engineering formal metatheory, (), 3-15 · Zbl 1295.68052
[5] Baader, F.; Nipkow, T., Term rewriting and all that, (1998), Cambridge University Press
[6] Basin, D., Verification of combinational logic in nuprl., Lecture notes in computer science, 408, 333-357, (July 1989)
[7] R. Bloo and K. H. Rose. Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In Computer Science in the Netherlands, November 1995.
[8] R. Bündgen, C. Sinz, and J. Walter. Redux 1.5: New facets of rewriting. In Ganzinger [17], pages 412-415.
[9] Constable, R., Implementing mathematics with the NUPRL development system, (1986), Prentice-Hall
[10] E. Contejean and C. Marché. CiME: Completion Modulo E. In Ganzinger [17], pages 416-419. System Description available at http://cime.lri.fr/.
[11] The Coq Development Team. The Coq Proof Assistant Reference Manual Version 8.2. INRIA-Rocquencourt, 2008.
[12] David, R.; Guillaume, B., A lambda-calculus with explicit weakening and explicit substitution, Mathematical structures in computer science, 11, 1, 169-206, (2001) · Zbl 0972.68028
[13] de Bruijn, N.G., Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation with application to the church-rosser theorem, Indag. mat., 34, 5, 381-392, (1972) · Zbl 0253.68007
[14] de Moura, F.L.C.; Ayala-Rincón, M.; Kamareddine, F., SUBSEXPL: A framework for simulating and comparing explicit substitutions calculi, Journal of applied and non-classical logics, 16, 1-2, 119-150, (2006) · Zbl 1184.68469
[15] de Moura, F.L.C.; Ayala-Rincón, M.; Kamareddine, F., Higher-order unification: A structural relation between huetʼs method and the one based on explicit substitutions, Journal of applied logic, 6, 1, 72-108, (2008) · Zbl 1138.03014
[16] de Moura, F.L.C.; Kamareddine, F.; Ayala-Rincón, M., Second order matching via explicit substitutions, (), 433-448 · Zbl 1108.03308
[17] ()
[18] T. Hardin and J.-J. Lévy. A Confluent Calculus of Substitutions. France-Japan Artificial Intelligence and Computer Science Symposium, December 1989.
[19] Huet, G., An analysis of böhmʼs theorem, Tcs, 121, 145-167, (1993) · Zbl 0794.03022
[20] ()
[21] Kamareddine, F.; Nederpelt, R.P., On stepwise explicit substitution, International journal of foundations of computer science, 4, 3, 197-240, (1993) · Zbl 0806.03013
[22] Kamareddine, F.; Nederpelt, R.P., A useful λ-notation, Tcs, 155, 85-109, (1996) · Zbl 0873.03018
[23] Kamareddine, F.; Ríos, A., A λ-calculus à la de Bruijn with explicit substitutions, (), 45-62
[24] Kamareddine, F.; Ríos, A., Relating the λσ- and λs-styles of explicit substitutions, Journal of logic and computation, 10, 3, 349-380, (2000) · Zbl 0953.03013
[25] Kawaguchi, N.; Sakabe, T.; Inagaki, Y., Terse: A visual environment for supporting analysis, verification and transformation of term rewriting systems, (), 571-574
[26] Kesner, D., A theory of explicit substitutions with safe and full composition, Logical methods in computer science, 5, 3:1, 1-29, (2009) · Zbl 1168.68008
[27] Lins, R., A new formula for the execution of a categorical combinators, (), 89-98 · Zbl 0642.68030
[28] Melliès, P.-A., Typed λ-calculi with explicit substitutions may not terminate, () · Zbl 1063.03522
[29] A. Mendelzon, A. Ríos, and B. Ziliani. Swapping: a natural bridge between named and indexed explicit substitution calculi. In 5th International Workshop on Higher-Order Rewriting - HOR 2010, pages 41-46, 2010.
[30] Milner, R.; Tofte, M.; Harper, R., The definition of standard ML, (1991), MIT Press Cambridge, MA
[31] Nadathur, G., A fine-grained notation for lambda terms and its use in intensional operations, J.of func. and logic programming, 1999, 2, 1-62, (1999) · Zbl 0924.68055
[32] Nederpelt, R.P.; Geuvers, J.H.; de Vrijer, R.C., Selected papers on automath, (1994), North-Holland · Zbl 0822.03009
[33] Nipkow, T.; Paulson, L.C.; Wenzel, M., Isabelle/HOL - A proof assistant for higher-order logic, () · Zbl 0994.68131
[34] Rose, K.H., Explicit cyclic substitutions, (), 36-50
[35] X. Leroy et. al. The Objective Caml system - release 3.11. Technical report, INRIA, 2008.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.