Lambda calculi with algebraic data types lie at the core of functional programming languages and proof assistants, but conceal at least two fundamental theoretical problems already in the presence of the simplest non-trivial data type, the sum type. First, we do not know of an explicit and implemented algorithm for deciding the beta-eta-equality of terms---and this in spite of the first decidability results proven two decades ago. Second, it is not clear how to decide when two types are essentially the same, i.e. isomorphic, in spite of the meta-theoretic results on decidability of the isomorphism.

While writing programs in continuation-passing style (CPS) is a common technique from Programming Languages research, writing mathematical proofs in CPS is much less common. Although such proofs open new possibilities for writing constructive proofs (for cases where more direct CPS-less proofs are not known, like in this tutorial), working with them is delicate (instead of data, we manipulate functionals). Proof assistants come to our rescue.