A temporal-logic approach to binding-time analysis

The Curry-Howard isomorphism identifies proofs with typed λ-calculus terms, and correspondingly identifies propositions with types. We show how this isomorphism can be extended to relate constructive temporal logic with binding-time analysis. In particular we show how to extend the Curry-Howard isomorphism to include the O (“next”) operator from linear-time temporal logic. This yields the simply typed λ^O-calculus which we prove to be equivalent to a multi-level binding-time analysis like those used in partial evaluation for functional programming languages. Further, we prove that normalization in λ^O can be done in an order corresponding to the times in the logic, which explains why λ^O is relevant to partial evaluation. We then extend λ^O to a small functional language, Mini-ML^O, and give an operational semantics for it. Finally, we prove that this operational semantics correctly reflects the binding-times in the language, a theorem which is the functional programming analog of time-ordered normalization