Mathematics and Computation

A blog about mathematics for computers

Sheaf Toposes for Realizability

with Steve Awodey.

Abstract: We compare realizability models over partial combinatory algebras by embedding them into sheaf toposes. We then use the machinery of Grothendieck toposes and geometric morphisms to study the relationship between realizability models over different partial combinatory algebras. This research is part of the Logic of Types and Computation project at Carnegie Mellon University under the direction of Dana Scott.

Sumitted for publication.

Download: sheaves_realizability.pdf,

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention, I will gladly respond. You are also welcome to contact me directly.