Loading...
Please wait, while we are loading the content...
Similar Documents
A Temporal-Logic Approach to Binding-Time Analysis (1995)
| Content Provider | CiteSeerX |
|---|---|
| Author | Davies, Rowan |
| Description | In Proceedings, 11 th Annual IEEE Symposium on Logic in Computer Science 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 fl ("next") operator from linear-time temporal logic. This yields the simply typed fl -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 fl can be done in an order corresponding to the times in the logic, which explains why fl is relevant to partial evaluation. We then extend fl to a small functional language, Mini-ML fl , and give an operational semantics for it. Finally, we prove that this operational semantics correctly reflects the bindingtimes in the language, a theorem which is the functional programming a... |
| File Format | |
| Language | English |
| Publisher | IEEE Computer Society Press |
| Publisher Date | 1995-01-01 |
| Access Restriction | Open |
| Subject Keyword | Curry-howard Isomorphism Mini-ml Fl Typed Calculus Term Small Functional Language Binding-time Analysis Partial Evaluation Functional Programming Language Typed Fl Calculus Curry-howard Isomorphism Identifies Identifies Proposition Operational Semantics Functional Programming Temporal-logic Approach Constructive Temporal Logic Linear-time Temporal Logic Multi-level Binding-time Analysis |
| Content Type | Text |
| Resource Type | Article |
