We found a match
Your institution may have rights to this item. Sign in to continue.
- Title
A typed lambda-calculus with first-class configurations.
- Authors
Abe, Tatsuya; Kimura, Daisuke
- Abstract
Filinski and Griffin have independently succeeded in extending the formulae-as-types notion to deal with continuations. Whereas Griffin adopted control operators primitively, Filinski adopted the duality of functions to construct a symmetric lambda-calculus in which continuations are first-class objects. In this paper, we construct a typed lambda-calculus with first-class configurations consisting of expressions and continuations of the same types. Our calculus corresponds to a natural deduction based on Rumfitt's bilateralism. Function types are represented as the implication and but-not connectives in intuitionistic and paraconsistent logics, respectively. Our calculus is not only logically consistent, but also computationally consistent. Our calculus with call-by-value and call-by-name strategies correspond to Wadler's call-by-value and call-by-name dual calculi, respectively. Furthermore, we propose a notion of relaxed configurations, which loosely take expressions and continuations of different types. We confirm that the relaxedness defines control operators for delimited continuations.
- Subjects
SYMMETRIC functions; CONTINUATION methods; CALCULI
- Publication
Journal of Logic & Computation, 2023, Vol 33, Issue 7, p1527
- ISSN
0955-792X
- Publication type
Article
- DOI
10.1093/logcom/exac062