Partial combinatory algebras and realizability interpretations of arithmetic, in Coq.
This was my master's thesis project in mathematics.
Thesis: http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-174109
(Direct link to pdf: http://kth.diva-portal.org/smash/get/diva2:858615/FULLTEXT01.pdf)