A Temporal-Logic Approach to Binding-Time Analysis

  • Rowan Davies


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.

How to Cite
Davies, R. (1995). A Temporal-Logic Approach to Binding-Time Analysis. BRICS Report Series, 2(51). https://doi.org/10.7146/brics.v2i51.19952