A Temporal-Logic Approach to Binding-Time Analysis
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.
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.