Abstract:
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 
(``next'')
operator from linear-time temporal logic. This yields the simply typed
-calculus which we prove to be equivalent to a multi-level
binding-time analysis like those used in partial evaluation.
Available as PostScript, PDF, DVI.