Mass problems and intuitionistic higher-order logic
Sankha S. Basu, Stephen G. Simpson · Computability · 2016
In this paper we study a model of intuitionistic higher-order logic which we call the Muchnik topos . The Muchnik topos may be defined briefly as the category of sheaves of sets over the topological space consisting of the Turing degrees, where the T