Both in proof search and proof theory certain paraproofs show up, ie derivations where some leaves are not justified by axioms but by authority. These justifications by authority rather serve the purpose of error elements known from programming. These paraproofs do not serve in general the purpose of establishing truths but rather are used for testing the real proofs.

This is basic to Girard's Ludics programme. But paraproofs also appear in recent work of Krivine and Danos on realizability for classical AF2 and in Curien and Herbelin's Duality of Computation where paraproofs appear as continuation terms. We leave it as a question for future investigations to find out whether paraproofs may provide a bridge between the fields of proof search and continuation semantics.