Spinal Atomic Lambda-Calculus

We present the spinal atomic [Formula: see text] -calculus, a typed [Formula: see text] -calculus with explicit sharing and atomic duplication that achieves spinal full laziness: duplicating only the direct paths between a binder and bound variables is enough for beta reduction to proceed. We show t...

Descripción completa

Detalles Bibliográficos
Autores principales: Sherratt, David, Heijltjes, Willem, Gundersen, Tom, Parigot, Michel
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7788627/
http://dx.doi.org/10.1007/978-3-030-45231-5_30
_version_ 1783633067519246336
author Sherratt, David
Heijltjes, Willem
Gundersen, Tom
Parigot, Michel
author_facet Sherratt, David
Heijltjes, Willem
Gundersen, Tom
Parigot, Michel
author_sort Sherratt, David
collection PubMed
description We present the spinal atomic [Formula: see text] -calculus, a typed [Formula: see text] -calculus with explicit sharing and atomic duplication that achieves spinal full laziness: duplicating only the direct paths between a binder and bound variables is enough for beta reduction to proceed. We show this calculus is the result of a Curry–Howard style interpretation of a deep-inference proof system, and prove that it has natural properties with respect to the [Formula: see text] -calculus: confluence and preservation of strong normalisation.
format Online
Article
Text
id pubmed-7788627
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-77886272021-01-07 Spinal Atomic Lambda-Calculus Sherratt, David Heijltjes, Willem Gundersen, Tom Parigot, Michel Foundations of Software Science and Computation Structures Article We present the spinal atomic [Formula: see text] -calculus, a typed [Formula: see text] -calculus with explicit sharing and atomic duplication that achieves spinal full laziness: duplicating only the direct paths between a binder and bound variables is enough for beta reduction to proceed. We show this calculus is the result of a Curry–Howard style interpretation of a deep-inference proof system, and prove that it has natural properties with respect to the [Formula: see text] -calculus: confluence and preservation of strong normalisation. 2020-04-17 /pmc/articles/PMC7788627/ http://dx.doi.org/10.1007/978-3-030-45231-5_30 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Sherratt, David
Heijltjes, Willem
Gundersen, Tom
Parigot, Michel
Spinal Atomic Lambda-Calculus
title Spinal Atomic Lambda-Calculus
title_full Spinal Atomic Lambda-Calculus
title_fullStr Spinal Atomic Lambda-Calculus
title_full_unstemmed Spinal Atomic Lambda-Calculus
title_short Spinal Atomic Lambda-Calculus
title_sort spinal atomic lambda-calculus
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7788627/
http://dx.doi.org/10.1007/978-3-030-45231-5_30
work_keys_str_mv AT sherrattdavid spinalatomiclambdacalculus
AT heijltjeswillem spinalatomiclambdacalculus
AT gundersentom spinalatomiclambdacalculus
AT parigotmichel spinalatomiclambdacalculus

Ejemplares similares