EVA STAR Trefferanzeige

Volltext Volltext.pdf1.pdf (456 KB)
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:swb:90-AAA435962
Titel Separating weakening and contraction in a linear lambda calculus.
Autor Maraist, John
Institution Fakultät für Informatik (INFORMATIK)
Institut für Programmstrukturen und Datenorganisation (IPD)
Dokumenttyp Buch
Jahr 1996
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,25.)
Abstract
We present a separated-linear lambda calculus based on a
refinement of linear logic which allows separate control of
weakening and contraction. The calculus satisfies subject reduction
and confluence, has a straightforward notion of standard evaluation,
and inherits previous results on the relationship of Girard's two
translations from minimal intuitionistic logic to linear logic with
call-by-name and call-by-value. We construct a hybrid translation from
Girard's two which is sound and complete for mapping types, reduction
sequences and standard evaluation sequences from call-by-need into
separated-linear lambda, a more satisfying treatment of call-by-need
than in previous work, which now allows a contrasting of all three
reduction strategies in the manner (for example) that the CPS transla-
tions allow for call-by-name and call-by-value.