### Abstract

An explicit-sharing lambda-calculus is presented, based on a Curry-Howard-style interpretation of the deep inference proof formalism. Duplication of subterms during reduction proceeds `atomically', i.e. on individual constructors, similar to optimal graph reduction in the style of Lamping. The calculus preserves strong normalisation with respect to the lambda-calculus, and achieves fully lazy sharing.

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

Title of host publication | Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science |

Subtitle of host publication | LICS'13 |

Publisher | IEEE |

Pages | 311-320 |

Number of pages | 10 |

ISBN (Print) | 9781479904136 |

DOIs | |

Publication status | Published - 1 Aug 2013 |

Event | Twenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013) - New Orleans, USA United States Duration: 24 Jun 2013 → 27 Jun 2013 |

### Publication series

Name | ACM/IEEE Symposium on Logic in Computer Science |
---|---|

Publisher | ACM/IEEE |

ISSN (Print) | 1043-6871 |

### Conference

Conference | Twenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013) |
---|---|

Country | USA United States |

City | New Orleans |

Period | 24/06/13 → 27/06/13 |

## Fingerprint Dive into the research topics of 'Atomic lambda-calculus: A typed lambda-calculus with explicit sharing'. Together they form a unique fingerprint.

## Cite this

Gundersen, T., Heijltjes, W., & Parigot, M. (2013). Atomic lambda-calculus: A typed lambda-calculus with explicit sharing. In

*Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science: LICS'13*(pp. 311-320). (ACM/IEEE Symposium on Logic in Computer Science). IEEE. https://doi.org/10.1109/LICS.2013.37