Back to Search
Start Over
Chapter 5: Logical Relations for Call-by-value Delimited Continuations.
- Source :
- Trends in Functional Programming Volume 6; 2007, Vol. 6, p63-78, 16p
- Publication Year :
- 2007
-
Abstract
- Logical relations, defined inductively on the structure of types, provide a powerful tool to characterize higher-order functions. They often enable us to prove correctness of a program transformer written with higher-order functions concisely. This paper demonstrates that the technique of logical relations can be used to characterize call-by-value functions as well as delimited continuations. Based on the traditional logical relations for call-by-name functions, logical relations for call-by-value functions are first defined, whose CPS variant is used to prove the correctness of an offline specializer for the call-by-value λ- calculus. They are then modified to cope with delimited continuations and are used to establish the correctness of an offline specializer for the call-by-value λ- calculus with delimited continuation constructs, shift and reset. This is the first correctness proof for such a specializer. Along the development, correctness of the continuation-based and shift/reset-based let-insertion and A-normalization is established. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISBNs :
- 9781841501765
- Volume :
- 6
- Database :
- Complementary Index
- Journal :
- Trends in Functional Programming Volume 6
- Publication Type :
- Book
- Accession number :
- 26215076