Simply typed lambda calculus with opposite types (2022)
ABSTRACT: In this article we present an extension of simply typed lambda calculus by introducing the idea of opposite types developed by Agudelo-Agudelo and Sicard-Ramírez (2021). The rules for these new types are based on the rules of a fragment of the logic system presented by the same authors. Two of the main properties of type systems are proven: The strong normalization theorem and the Curry-Howard correspondence.