Logic in Computer Science (LICS 1996)

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}
  }