LFCS seminar: Peter Dybjer

Program testing and constructive validity

Peter Dybjer, Chalmers University of Technology, Sweden.

Abstract: In this talk I shall argue that program testing provides the basis for mathematical truth, and that mathematics is an empirical science. This point of view is the result of an analysis of Martin-L\"of's meaning explanations for intuitionistic type theory, where the judgements of type theory are viewed as conjectures which can be tested in order to be corroborated or refuted. One consequence is a new perspective of hypothetical judgments, since tests for such judgments need methods for generating inputs.  Among other things, we need to generate function input. The continuity principle is relevant here and it follows that the alleged impredicativity of functionals can be rejected. Furthermore, our testing semantics suggests that we should only allow the formation of identity types over decidable types.  At the end we turn to impredicative type theory, and discuss possible testing semantics for such theories. In particular we propose that testing for impredicative type theory should be based on the evaluation of open expressions rather than of closed expressions as for predicative type theory.