Realizability in Coq
Anders Lundstedt · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2015
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.