Abstract:

The talk reviews some basic proof theoretic results
on realizability, as well as the construction of an elementary
topos which generalizes realizability as a semantics for
intuitionistic type theory.
We see that the proof theoretic result of "idempotency of
formalized realizability" has a semantic counterpart in this topos;
we derive a theory in higher order arithmetic which is complete
for realizability (and which is valid in the topos); using this we
can give a very elementary proof of a completeness property of
the category of PERs.
 

Back to Talks Page