A Temporal-Logic Approach to Binding-Time Analysis

Abstract

The Curry-Howard isomorphism identifies proofs with typed lambda-
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   ("next") operator from linear-time temporal
logic. This yields the simply typed lambda-calculus which we prove
to be equivalent to a multi-level binding-time analysis like those
used in partial evaluation.

Keywords: Curry-Howard isomorphism, partial evaluation, binding-time analysis, temporal logic.