A Temporal-Logic Approach to Binding-Time Analysis

Rowan Davies

October 1995


The Curry-Howard isomorphism identifies proofs with typed tex2html_wrap_inline19 -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 tex2html_wrap_inline21 (``next'') operator from linear-time temporal logic. This yields the simply typed tex2html_wrap_inline23 -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.


Last modified: 2003-06-08 by webmaster.