  The first idea goes back to the Curry-Howard correspondence (see de Groote, 1995; Sørensen and Urzyczyn, 2006), according to which the fact that a formula A has a certain proof can be codified as the fact that a certain term t is of type A, whereby the formula A is identified with the type A. This can be formalized in a calculus for type assignment, whose statements are of the form t : A. A proof of t : A in this system can be read as showing that t is a proof of A. Martin-Löf (1995; 1998) has put this into a philosophical perspective by distinguishing this two-fold sense of proof in the following way. First we have proofs of statements of the form t : A. These statements are called judgements, their proofs are called demonstrations. Within such judgements the term t represents a proof of the proposition A. A proof in the latter sense is also called a proof object. When demonstrating a judgement t : A, we demonstrate that t is a proof (object) for the proposition A. Within this two-layer system the demonstration layer is the layer of argumentation. Unlike proof objects, demonstrations have epistemic significance; their judgements carry assertoric force. The proof layer is the layer at which meanings are explained: The meaning of a proposition A is explained by telling what counts as a proof (object) for A. The distinction made between canonical and non-canonical proofs is a distinction at the propositional and not at the judgement al layer. This implies a certain explicitness requirement. When I have proved something, I must not only have a justification for my proof at my disposal as in Prawitz’s notion of validity, but at the same time have to be certain that this justification fulfills its purpose. This certainty is guaranteed by a demonstration. Mathematically, this two-fold sense of proof develops its real power only when types may themselves depend on terms. Dependent types are a basic ingredient of of Martin-Löf’s type theory and related approaches.