Proofs, lambda terms and control operators
The so-called continuation-passing-style translation (cps-translation) has been introduced by \textit{M. Fischer} [``Lambda calculus schemata, Sigplan Notices 7, 104-109 (1972)] for the \(\lambda\)-calculus and extended to the \(\lambda\)-calculus with control operators \({\mathcal C}\) and \({\mathcal A}\) by \textit{M. Felleisen}, \textit{D. P. Friedman}, \textit{E. Kohlbecker} and \textit{B. Duba} [Theor. Comput. Sci. 52, 205-237 (1987; Zbl 0643.03011)]. By giving a typing, a connection with implicational propositional logic has been established by \textit{A. R. Meyer} and \textit{M. Wand} [Lect. Notes Comput. Sci. 193, 219-224 (1985; Zbl 0565.68028)] for the \(\lambda\)-calculus and extended to the \(\lambda\)-calculus with control operators \({\mathcal C}\) and \({\mathcal A}\) by \textit{T. G. Griffin} [``A formulae-as-types notion of control, Conf. Rec. 17th Ann. ACM Symp. Principles Program. Lang., 47-58 (1990)]. Griffin has shown that all evaluations with respect to call-by-value \(\beta\)-conversion and the standard conversion rules for \({\mathcal C}\) and \({\mathcal A}\) terminate. More precisely Griffin extends the Meyer/Wand typing of Fischer's cps-translation \(\overline M\) of a term \(M\) to the language involving the control operators \({\mathcal C}\) and \({\mathcal A}\). It still holds that if \(M\) has type \(A\), then \(\overline M\) has type \(\neg \neg A^0\), where \(A^0\) is defined as \(P^0:=P\) and \((A\to B)^0: =A^0\to \neg B^0 \to \text{F}\) (which is equivalent to \(\neg B^0 \to \neg A^0)\). Griffin's proof of termination of evaluation is based on \textit{G. D. Plotkin}'s [Theor. Comput. Sci. 1, 125-159 (1975; Zbl 0325.68006)] technique of the so-called colon-translation (denoted \(M:V\) and typed by \(M^A: V^{\neg A^0})\) and context unwrapping (denoted by \(V^E\) and typed by requiring \(V\) to be of type \(\neg B^0\), and the evaluation context \(E\square\) to be of type \(B\) with the `hole' of type \(A)\). Here we essentially give an exposition of Griffin's result, with some simplifications and extensions based on work of \textit{A. Sabry} and \textit{M. Felleisen} [``Reasoning about programs in continuation-passing style, Lisp Symb. Comput. 6, 289-360 (1993)]. In particular we stress its connection with questions of termination of different normalization strategies for minimal, intuitionistic and classical logic, or more precisely their fragments in implicational propositional logic. We also give some examples (due to Hirokawa) of derivations in minimal and classical logic which reproduce themselves under certain reasonable conversion rules. For the entire collection see [Zbl 0869.00051].
- Non-strictly positive fixed points for classical natural deduction
- Comparing control constructs by double-barrelled CPS
- Continuation-passing style models complete for intuitionistic logic
- A higher-order colon translation
- A context-based approach to proving termination of evaluation
- Proofs, tests and continuation passing style
- A proof theoretical account of continuation passing style
- scientific article; zbMATH DE number 2053247 (Why is no real title available?)
- Comparing control constructs by double-barrelled CPS transforms
- A CPS-translation of the -calculus
- Proving termination of evaluation for system F with control operators
- Constructive classical logic as CPS-calculus
- Strong normalization proofs by CPS-translations
This page was built for publication: Proofs, lambda terms and control operators
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4357067)
