Reversible, Irreversible and Optimal λ-machines: Extended abstract

Vincent Danos; Laurent Regnier

doi:10.1016/S1571-0661(05)80402-5

Reversible, Irreversible and Optimal λ-machines: Extended abstract

Research output: Contribution to journal › Article › peer-review

Abstract

There are two quite different possibilities for implementing linear head reduction in λ-calculus. Two ways which we are going to explain briefly here in the introduction and in details in the body of the paper. The paper itself is concerned with showing an unexpectedly simple relation between these two ways, which we term reversible and irreversible, namely that the latter may be obtained as a natural optimization of the former.

Original language	English
Pages (from-to)	40 - 60
Number of pages	21
Journal	Electronic Notes in Theoretical Computer Science
Volume	3
DOIs	https://doi.org/10.1016/S1571-0661(05)80402-5
Publication status	Published - 1996

Keywords / Materials (for Non-textual outputs)

reversible computations
λ-calculus
abstract machines
geometry of interaction

Access to Document

10.1016/S1571-0661(05)80402-5

Reversible, Irreversible and Optimal λ-machines. Extended abstract
Open Access document
Final published version, 941 KB

http://www.sciencedirect.com/science/article/pii/S1571066105804025

Cite this

@article{a9e73666cf5c4d55bb8728037da2af95,

title = "Reversible, Irreversible and Optimal λ-machines: Extended abstract",

abstract = "There are two quite different possibilities for implementing linear head reduction in λ-calculus. Two ways which we are going to explain briefly here in the introduction and in details in the body of the paper. The paper itself is concerned with showing an unexpectedly simple relation between these two ways, which we term reversible and irreversible, namely that the latter may be obtained as a natural optimization of the former.",

keywords = "reversible computations, λ-calculus, abstract machines, geometry of interaction",

author = "Vincent Danos and Laurent Regnier",

note = "Linear Logic 96 Tokyo Meeting",

year = "1996",

doi = "10.1016/S1571-0661(05)80402-5",

language = "English",

volume = "3",

pages = "40 -- 60",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

}

TY - JOUR

T1 - Reversible, Irreversible and Optimal λ-machines: Extended abstract

AU - Danos, Vincent

AU - Regnier, Laurent

N1 - Linear Logic 96 Tokyo Meeting

PY - 1996

Y1 - 1996

N2 - There are two quite different possibilities for implementing linear head reduction in λ-calculus. Two ways which we are going to explain briefly here in the introduction and in details in the body of the paper. The paper itself is concerned with showing an unexpectedly simple relation between these two ways, which we term reversible and irreversible, namely that the latter may be obtained as a natural optimization of the former.

AB - There are two quite different possibilities for implementing linear head reduction in λ-calculus. Two ways which we are going to explain briefly here in the introduction and in details in the body of the paper. The paper itself is concerned with showing an unexpectedly simple relation between these two ways, which we term reversible and irreversible, namely that the latter may be obtained as a natural optimization of the former.

KW - reversible computations

KW - λ-calculus

KW - abstract machines

KW - geometry of interaction

U2 - 10.1016/S1571-0661(05)80402-5

DO - 10.1016/S1571-0661(05)80402-5

M3 - Article

SN - 1571-0661

VL - 3

SP - 40

EP - 60

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Reversible, Irreversible and Optimal λ-machines: Extended abstract

Abstract

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this