A semantics and a sequent calculus for dual counterpart intuitionistic logic

The property of logical duality arises most clearly within classical logic (or CL), and as a result it contributes to some of the aspects of the programs that correspond to the proofs of CL under the Curry-Howard correspondence. Specifically, a program that can be assigned a classical type can naturally exhibit useful programming features that are not present in other settings of the Curry-Howard correspondence. These features include control effects that can induce exception-like changes to the program context; encodings of coinductive datatypes that facilitate elegant support for datatypes such as streams or circular lists; and support for multiple program evaluation strategies within the same language. Despite these desirable features, CL is not constructive and so therefore it is problematic to use it as a type-theoretic foundation for a theorem proving system. Intuitionistic logic (or Int) is constructive and so it is the typical choice of foundation for such a system. However, Int fundamentally lacks the logical duality of CL. The bi-intuitionistic logic of Rauszer (or BiInt) is a well known extension of Int that does have duality. However, a critical point of dissimilarity to Int is that BiInt is not constructive. This dissertation contributes a new constructive logic called dual-counterpart intuitionistic logic (or DCInt) that is an extension of Int, has duality, and is a sublogic of BiInt. This logic combines desirable features of both CL and Int while remaining conservative with respect to BiInt, and this means that it may have useful applications under the Curry-Howard correspondence. It establishes both the semantics and the proof theory of the logic, and also proves that the logic is constructive. Additionally, it investigates the similarities and differences between DCInt and other known logics that are constructive and have duality.