Internalizing the sequent calculus dualities
Gentzen’s sequent calculus is a foundation of modern logic and, more recently, programming language design. It is known for being more symmetric than natural deduction, a deduction calculus that is biased on proofs and truth, whereas sequent calculus does symmetrically support proofs/truth and refutations/falsity.
However, the way sequent calculus is usually defined, those symmetries have to be observed and proved after the fact, as opposed to be an inherent part of the calculus.
Our research group has developed a method of syntactically abstracting over so-called polarities and orientations. The task of this thesis is to 1) apply this method to the sequent calculus and Herbelin’s programming calculus based on the sequent calculus, and 2) validating the new formulation by showing that proofs and programs can be “polymorphic” in their polarity and orientation.