  In this paper I will develop a lambda-term calculus, lambda-2Int, for a
bi-intuitionistic logic and discuss its implications for the notions of sense
and denotation of derivations in a bilateralist setting. Thus, I will use the
Curry-Howard correspondence, which has been well-established between the simply
typed lambda-calculus and natural deduction systems for intuitionistic logic,
and apply it to a bilateralist proof system displaying two derivability
relations, one for proving and one for refuting. The basis will be the natural
deduction system of Wansing's bi-intuitionistic logic 2Int, which I will turn
into a term-annotated form. Therefore, we need a type theory that extends to a
two-sorted typed lambda-calculus. I will present such a term-annotated proof
system for 2Int and prove a Dualization Theorem relating proofs and refutations
in this system. On the basis of these formal results I will argue that this
gives us interesting insights into questions about sense and denotation as well
as synonymy and identity of proofs from a bilateralist point of view.
