## Paper: A temporal-logic approach to binding-time analysis (at LICS 1996)

Authors:**Rowan Davies**

### Abstract

The Curry-Howard isomorphism identifies proofs with typed /spl 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 O ("next") operator from linear-time temporal logic. This yields the simply typed /spl lambda//sup O/-calculus which we prove to be equivalent to a multi-level binding-time analysis like those used in partial evaluation for functional programming languages. Further, we prove that normalization in /spl lambda//sup O/ can be done in an order corresponding to the times in the logic, which explains why /spl lambda//sup O/ is relevant to partial evaluation. We then extend /spl lambda//sup O/ to a small functional language, Mini-ML/sup O/, and give an operational semantics for it. Finally, we prove that this operational semantics correctly reflects the binding-times in the language, a theorem which is the functional programming analog of time-ordered normalization.

### BibTeX

@InProceedings{Davies-Atemporallogicappro, author = {Rowan Davies}, title = {A temporal-logic approach to binding-time analysis}, booktitle = {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996}, year = 1996, editor = {Edmund M. Clarke}, month = {July}, pages = {184-195}, location = {New Brunswick, NJ, USA}, publisher = {IEEE Computer Society Press} }