Downloads provided by UsageCounts
handle: 1822/39302
This paper tries to remove what seems to be the remaining stumbling blocks in the way to a full understanding of the Curry-Howard isomorphism for sequent calculus, namely the questions: What do variables in proof terms stand for? What is co-control and a co-continuation? How to define the dual of Parigot's mu-operator so that it is a co-control operator? Answering these questions leads to the interpretation that sequent calculus is a formal vector notation with first-class co-control. But this is just the "internal" interpretation, which has to be developed simultaneously with, and is justified by, an equivalent, "external" interpretation, offered by natural deduction: the sequent calculus corresponds to a bi-directional, agnostic (w.r.t. the call strategy), computational lambda-calculus. Next, the formal duality between control and co-control is studied, in the context of classical logic. The duality cannot be observed in the sequent calculus, but rather in a system unifying sequent calculus and natural deduction.
Computational lambda-calculus, de Morgan duality, Vector notation, co-continuation, vector notation, Co-control, context substitution, Formal substitution, computational lambda-calculus, 004, classical lo, let-expression, Context substitution, Co-continuation, Classical logic, Let-expression, formal sub- stitution, co-control, ddc: ddc:004
Computational lambda-calculus, de Morgan duality, Vector notation, co-continuation, vector notation, Co-control, context substitution, Formal substitution, computational lambda-calculus, 004, classical lo, let-expression, Context substitution, Co-continuation, Classical logic, Let-expression, formal sub- stitution, co-control, ddc: ddc:004
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| views | 2 | |
| downloads | 1 |

Views provided by UsageCounts
Downloads provided by UsageCounts