Metodo

International Studies in Phenomenology and Philosophy

Book | Chapter

186519

Program testing and the meaning explanations of intuitionistic type theory

Peter Dybjer

pp. 215-241

Abstract

The relationship between program testing and Martin-Löf"s meaning explanations for intuitionistic type theory is investigated. The judgements of intuitionistic type theory are viewed as conjectures which can be tested in order to be corroborated or refuted. This point of view provides a new perspective on the meaning of hypothetical judgements, since tests for such judgements need methods for generating inputs. Among other things, we need to generate function input. The continuity principle is invoked and the impredicativity of types of functionals is rejected. Furthermore, we provide testing semantics only for decidable identity types. At the end we turn to impredicative type theories, 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. This is in contrast to our testing semantics for Martin-Löf"s predicative intuitionistic type theory which is based on the evaluation of closed expressions.

Publication details

Published in:

Dybjer P, Lindström Sten, Palmgren Erik, Sundholm Göran (2012) Epistemology versus ontology: essays on the philosophy and foundations of mathematics in honour of per Martin-löf. Dordrecht, Springer.

Pages: 215-241

DOI: 10.1007/978-94-007-4435-6_11

Full citation:

Dybjer Peter (2012) „Program testing and the meaning explanations of intuitionistic type theory“, In: P. Dybjer, S. Lindström, E. Palmgren & G. Sundholm (eds.), Epistemology versus ontology, Dordrecht, Springer, 215–241.