A Typed Lambda-Calculus with First-Class Configurations A Typed Lambda-Calculus with First-Class Configurations

Tatsuya Abe and Daisuke Kimura. A Typed Lambda-Calculus with First-Class Configurations. Journal of Logic and Computation. DOI: 10.1093/logcom/exac062

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.