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.

Full Text:


DOI: http://dx.doi.org/10.7146/brics.v2i51.19952
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the State and University Library and Aarhus University Library