KIT | KIT-Bibliothek | Impressum | Datenschutz
Open Access Logo
URN: urn:nbn:de:swb:90-AAA435962

Separating weakening and contraction in a linear lambda calculus

Maraist, John


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.

Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Buch
Jahr 1996
Sprache Englisch
Identifikator KITopen ID: 43596
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,25.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page