This thesis describes a Coq formalization of realizability interpretations of arithmetic. The realizability interpretations are based on partial combinatory algebras—to each partial combinatory algebra there is an associated realizability interpretation. I construct two partial combinatory algebras. One of these gives a realizability interpretation equivalent to Kleene’s original one, without involving the usual recursion-theoretic machinery. / Den här uppsatsen beskriver en Coq-formalisering av realiserbarhetstolkningar av aritmetik. Realiserbarhetstolkningarna baseras på partiella kombinatoriska algebror—för varje partiell kombinatorisk algebra finns det en motsvarande realiserbarhetstolkning. Jag konstruerar två partiella kombinatoriska algebror. En av dessa ger en realiserbarhetstolkning som är ekvivalent med Kleenes ursprungliga tolkning, men dess konstruktion använder inte det sedvanliga rekursionsteoretiska maskineriet.

京都大学 / 新制・課程博士 / 博士(理学) / 甲第24393号 / 理博第4892号 / 新制||理||1699(附属図書館) / 京都大学大学院理学研究科数学・数理解析専攻 / (主査)教授 長谷川 真人, 教授 牧野 和久, 准教授 照井 一成 / 学位規則第4条第1項該当 / Doctor of Science / Kyoto University / DFAM