(Research notes are also available below.)
pdf , Agda version, slides.
pdf, Agda formalization (also as a zip file).
pdf.
pdf.
pdf.
pdf, Agda (with combinatory version of system T), Agda without comments, Agda using Church encoding of dialogues, Agda internalizing the modulus of continuity, Agda (with lambda-calculus version of system T), more.
pdf, Agda, A family of types that fail to be provably collapsible (also in Agda), Constant choice.
See also the companion programs/proofs in Agda.
pdf.
paper, slides presented at MAP'2011 in Leiden, draft full version (a more polished full version will be eventually available, for the moment the paper is more readable).
Electronically available as Technical Report 97:05, School of Cognitive and Computing Sciences, University of Sussex.
ECS-LFCS-97-374 (follow this link and then find file at the bottom).
zip file with Haskell programs and scripts.
There is also a literate program derived from this used for a talk in Fun in the Afternoon (March 2011).
pdf.
pdf.
pdf.