Projects per year

### Abstract

We present the spinal atomic lambda-calculus, a typed lambda-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 lambda-calculus: confluence and preservation of strong normalisation.

Original language | English |
---|---|

Pages | 582-601 |

DOIs | |

Publication status | Published - 2020 |

## Projects

- 1 Active

### Typed Lambda-Calculi with Sharing and Unsharing

Engineering and Physical Sciences Research Council

1/01/19 → 31/12/21

Project: Research council

## Cite this

Sherratt, D., Heijltjes, W., Gundersen, T., & Parigot, M. (2020).

*Spinal atomic lambda-calculus*. 582-601. https://doi.org/10.1007/978-3-030-45231-5_30