
COPLASCopenhagen Programming Language Seminar 
basis for mathematical truth, and that mathematics is an empirical science. This point of view is the result of an analysis of MartinL\"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. 
Scientific host:
Lars Birkedal Administrative host:Renée Korver Michan.
All are welcome.
The Copenhagen Programming
Language Seminar (COPLAS) is a collaboration between DIKU,
ITU and
RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to
proglangrequest@mail.itc.dk with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see
http://www.coplas.org