Meaning Explanations of Intutionistic Type Theory
Paper:
Slides:
- On the PhD thesis "Reference and
Computation in Intuitionistic Type Theory" by Johan Granström, Uppsala, January 2009.
- Program Testing and
Constructive Validity, presented at the Conference on Philosophy
and Foundations of Mathematics: Ontological and Epistemological
Aspects, Uppsala, May 2009.
- Tests, Games,
and Martin-Löf’s Meaning Explanations
for Intuitionistic Type Theory. Invited lecture at the
Meeting on
Logic and Interactions
CIRM, Marseille, 13 February 2012.
- Implementing Martin-Löf’s Meaning
Explanations in Agda, AIM XXI, Göteborg, June 2015.
Agda-files.