### Abstract

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 |

ISBN (Print) | 9781479904136 |

DOIs | |

Status | Published - Jun 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 |

### 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

### Cite this

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

**Atomic lambda-calculus : A typed lambda-calculus with explicit sharing.** / Gundersen, Tom; Heijltjes, Willem; Parigot, Michel.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science: LICS'13.*IEEE, pp. 311-320, Twenty-Eighth Annucal ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), New Orleans, USA United States, 24/06/13. DOI: 10.1109/LICS.2013.37

}

TY - GEN

T1 - Atomic lambda-calculus

T2 - A typed lambda-calculus with explicit sharing

AU - Gundersen,Tom

AU - Heijltjes,Willem

AU - Parigot,Michel

PY - 2013/6

Y1 - 2013/6

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84883443813&partnerID=8YFLogxK

UR - http://lii.rwth-aachen.de/lics/lics13/

UR - http://dx.doi.org/10.1109/LICS.2013.37

U2 - 10.1109/LICS.2013.37

DO - 10.1109/LICS.2013.37

M3 - Conference contribution

SN - 9781479904136

SP - 311

EP - 320

BT - Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science

PB - IEEE

ER -