TY  - UNPD
A1  - Schmidt-Schauß, Manfred
A1  - Sabel, David
T1  - On generic context lemmas for lambda calculi with sharing
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 27
N2  - This paper proves several generic variants of context lemmas and thus contributes to improving the tools for observational semantics of deterministic and non-deterministic higher-order calculi that use a small-step reduction semantics. The generic (sharing) context lemmas are provided for may- as well as two variants of must-convergence, which hold in a broad class of extended process- and extended lambda calculi, if the calculi satisfy certain natural conditions. As a guide-line, the proofs of the context lemmas are valid in call-by-need calculi, in callby-value calculi if substitution is restricted to variable-by-variable and in process calculi like variants of the π-calculus. For calculi employing beta-reduction using a call-by-name or call-by-value strategy or similar reduction rules, some iu-variants of ciu-theorems are obtained from our context lemmas. Our results reestablish several context lemmas already proved in the literature, and also provide some new context lemmas as well as some new variants of the ciu-theorem. To make the results widely applicable, we use a higher-order abstract syntax that allows untyped calculi as well as certain simple typing schemes. The approach may lead to a unifying view of higher-order calculi, reduction, and observational equality.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 27 [v.3] 
KW  - lambda calculus
KW  - observational semantics
KW  - context lemma
KW  - functional programming languages
Y1  - 2008
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34428
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-344287
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-27_v3.pdf
IS  - Version: 19 Juni 2008
EP  - 36
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik
CY  - Frankfurt am Main
ER  -