摘要

This article demonstrates that there is a fundamental relationship between temporal logic and languages that involve multiple stages, such as those used to analyze binding times in the context of partial evaluation. This relationship is based on an extension of the Curry-Howard isomorphism, which identifies proofs with programs, and propositions with types. Our extension involves the "next time" (circle) operator from linear-time temporal logic and yields a lambda-calculus. lambda degrees with types of the form circle A for expressions in the subsequent stage, with appropriate introduction and elimination forms. We demonstrate that. lambda degrees is equivalent to the core of a previously studied multilevel binding-time analysis. This is similar to work by Davies and Pfenning on staged computation based on the necessity (square) operator of modal logic, but square only allows closed code, and naturally supports a code evaluation construct, whereas circle captures open code, thus is more flexible, but is incompatible with such a construct. Instead, code evaluation is an external global operation that is validated by the proof theory regarding closed proofs of circle formulas. We demonstrate the relevance of lambda degrees to staged computation directly by showing that that normalization can be done in an order strictly following the times of the logic. We also extend. lambda degrees to small functional language and show that it would serve as a suitable basis for directly programming with multiple stages by presenting some example programs.

  • 出版日期2017-3