Directed virtual reductions

Vincent Danos, Marco Pedicini, Laurent Regnier

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

This note defines a new graphical local calculus, directed virtual reductions. It is designed to compute Girard's execution formula EX, an invariant of closed functional evaluation obtained from the “geometry of interaction” interpretation of λ-calculus [5].

The calculus is obtained by synchronizing another graphical local calculus presented in “local and asynchronous beta-reduction”: virtual reductions [4]. This synchronization makes it easier to mechanize than general virtual reductions. In undirected virtual reductions the consistency of the computation is insured by an algebraic mechanism called the bar. This mechanism in general induces correction terms of any order. The directed virtual reduction has been designed to keep those terms at order one.

A further synchronization, the combustion strategy will even wipe out first order correction terms. Applied to sharing graphs, the combustion strategy yields Lamping's optimal graphical calculus as presented in [1]. But more efficient optimal implementations of λ-calculus are expected.

The paper is conceived as a follow-up of [4] and supposes a familiarity with virtual reduction.
Original languageEnglish
Title of host publicationComputer Science Logic
Subtitle of host publication10th International Workshop, CSL '96 Annual Conference of the EACSL Utrecht, The Netherlands, September 21–27, 1996 Selected Papers
EditorsDirk van Dalen, Marc Bezem
PublisherSpringer Berlin Heidelberg
Number of pages13
ISBN (Electronic)978-3-540-69201-0
ISBN (Print)978-3-540-63172-9
Publication statusPublished - 1997

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'Directed virtual reductions'. Together they form a unique fingerprint.

Cite this