A Theory of Explicit Substitutions with Safe and Full Composition

Delia Kesner

doi:10.2168/LMCS-5(3:1)2009

Delia Kesner - A Theory of Explicit Substitutions with Safe and Full Composition

lmcs:816 - Logical Methods in Computer Science, July 15, 2009, Volume 5, Issue 3 - https://doi.org/10.2168/LMCS-5(3:1)2009

A Theory of Explicit Substitutions with Safe and Full CompositionArticle

Authors: Delia Kesner

Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the first part of this paper. Then, very simple technology in named variable-style notation is used to establish a theory of explicit substitutions for the lambda-calculus which enjoys a whole set of useful properties such as full composition, simulation of one-step beta-reduction, preservation of beta-strong normalisation, strong normalisation of typed terms and confluence on metaterms. Normalisation of related calculi is also discussed.

Comment: 29 pages Special Issue: Selected Papers of the Conference "International Colloquium on Automata, Languages and Programming 2008" edited by Giuseppe Castagna and Igor Walukiewicz

https://doi.org/10.2168/LMCS-5(3:1)2009

Source: arXiv.org:0905.2539

Volume: Volume 5, Issue 3

Secondary volumes: Selected Papers of the 35th International Colloquium on Automata, Languages and Programming (ICALP 2008)

Published on: July 15, 2009

Imported on: December 8, 2008

Keywords: Computer Science - Programming Languages, Computer Science - Logic in Computer Science, F.3.2, D.1.1, F.4.1

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

17 Documents citing this article

Felipe A. Costa;Daniel Ventura, 2025, Formal Development for a Node Replication Calculus with Abstract Machine Extraction for a Lazy Strategy, Anais do VI Workshop Brasileiro de Lógica (WBL 2025), pp. 16-23, 10.5753/wbl.2025.8267.

Pablo Barenbaum;Delia Kesner;Mariana Milicich, 2025, A Fresh Inductive Approach to Useful Call-by-Value, Lecture notes in computer science, pp. 381-399, 10.1007/978-3-031-99984-0_21, https://doi.org/10.1007/978-3-031-99984-0_21.

Philip Wadler, 2024, Explicit Weakening, Electronic Proceedings in Theoretical Computer Science, 413, pp. 15-26, 10.4204/eptcs.413.2, https://doi.org/10.4204/eptcs.413.2.

Balabonski, Thibaut;Lanco, Antoine;Melquiond, Guillaume, 2021, A Strong Call-By-Need Calculus, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 10.4230/lipics.fscd.2021.9, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.9.

Delia Kesner;Loïc Peyrot;Daniel Ventura, 2021, The Spirit of Node Replication, Lecture notes in computer science, pp. 344-364, 10.1007/978-3-030-71995-1_18, https://doi.org/10.1007/978-3-030-71995-1_18.

Xiaohong Chen;Grigore Roşu, 2020, A general approach to define binders using matching logic, Proceedings of the ACM on Programming Languages, 4, ICFP, pp. 1-32, 10.1145/3408970, https://doi.org/10.1145/3408970.

Benedikt Ahrens;André Hirschowitz;Ambroise Lafont;Marco Maggesi, 2019, Reduction monads and their signatures, Proceedings of the ACM on Programming Languages, 4, POPL, pp. 1-29, 10.1145/3371099, https://doi.org/10.1145/3371099.

ÁLVARO GARCÍA-PÉREZ;PABLO NOGUEIRA, 2019, The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus, Journal of Functional Programming, 29, 10.1017/s0956796819000017.

Thibaut Balabonski;Pablo Barenbaum;Eduardo Bonelli;Delia Kesner, 2017, Foundations of strong call by need, Proceedings of the ACM on Programming Languages, 1, ICFP, pp. 1-29, 10.1145/3110264, https://doi.org/10.1145/3110264.

Beniamino Accattoli;Pablo Barenbaum;Damiano Mazza, 2014, Distilling abstract machines, ACM SIGPLAN Notices, 49, 9, pp. 363-376, 10.1145/2692915.2628154.

Beniamino Accattoli;Pablo Barenbaum;Damiano Mazza, 2014, Distilling abstract machines, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pp. 363-376, 10.1145/2628136.2628154.

Delia Kesner;Daniel Ventura, 2014, Quantitative Types for the Linear Substitution Calculus, Lecture notes in computer science, pp. 296-310, 10.1007/978-3-662-44602-7_23, https://doi.org/10.1007/978-3-662-44602-7_23.

Beniamino Accattoli;Delia Kesner, 2012, Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus, Logical Methods in Computer Science, Volume 8, Issue 1, 10.2168/lmcs-8(1:28)2012, https://doi.org/10.2168/lmcs-8(1:28)2012.

Ariel Mendelzon;Alejandro Ríos;Beta Ziliani, 2011, Swapping: a natural bridge between named and indexed explicit substitution calculi, Electronic Proceedings in Theoretical Computer Science, 49, pp. 1-15, 10.4204/eptcs.49.1, https://doi.org/10.4204/eptcs.49.1.

F.L.C. de Moura;A.V. Barbosa;M. Ayala-Rincón;F. Kamareddine, 2011, A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi, Electronic Notes in Theoretical Computer Science, 269, pp. 41-54, 10.1016/j.entcs.2011.03.004, https://doi.org/10.1016/j.entcs.2011.03.004.

José Espírito Santo;Luís Pinto, 2011, A calculus of multiary sequent terms, ACM Transactions on Computational Logic, 12, 3, pp. 1-41, 10.1145/1929954.1929959, https://doi.org/10.1145/1929954.1929959.

Stefan Hetzl, 2010, A Sequent Calculus with Implicit Term Representation, Lecture notes in computer science, pp. 351-365, 10.1007/978-3-642-15205-4_28.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3226 times.

This article's PDF has been downloaded 987 times.