Copenhagen 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
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.
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 email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org