Paper Info

Title | ||
---|---|---|

A semantical storage operator theorem for all types |

Abstract | ||
---|---|---|

Storage operators are λ-terms which simulate call-by-value in call-by-name for a given set of terms. Krivine's storage operator theorem shows that any term of type ¬D → ¬D∗, where D∗ is the Gödel translation of D, is a storage operator for the terms of type D when D is a data-type or a formula with only positive second order quantifiers. We prove that a new semantical version of Krivine's theorem is valid for every types. This also gives a simpler proof of Krivine's theorem using the properties of data-types. |

Year | DOI | Venue |
---|---|---|

1998 | 10.1016/S0168-0072(97)00041-9 | Annals of Pure and Applied Logic |

Keywords | Field | DocType |

λ-calculus,Types,AF2 type system,Storage operators,Gödel translations | Discrete mathematics,Algebra,Gödel,Pure mathematics,Operator (computer programming),Mathematics | Journal |

Volume | Issue | ISSN |

91 | 1 | 0168-0072 |

Citations | PageRank | References |

1 | 0.39 | 7 |

Authors | ||

1 |

Authors (1 rows)

Cited by (1 rows)

References (7 rows)

Name | Order | Citations | PageRank |
---|---|---|---|

Christophe Raffalli | 1 | 29 | 5.55 |