The Curry-Howard isomorphism is a correspondence between logic and computation with applications ranging from philosophy of mathematics to software engineering. Technically, the isomorphism links proof systems and typed lambda-calculi, both at the syntactic/static and the semantic/dynamic levels. The isomorphism has two well-established versions, for Hilbert systems and systems of natural deduction, and one problematic case, when the proof system is taken to be the sequent calculus. In this seminar the two well-established instances of the isomorphism are recalled and the difficulties raised by the sequent calculus are revisited. Next, a new variant of the lambda-calculus is introduced, which can be described as a "formalized vector notation with first-class co-control". The main goal of the seminar is to make sense of this phrase and argue how and why this variant illuminates (solves?) the sequent calculus case.
 |