KnowledgeBase » 
SEMINAR
» ID = 742
Synthetic Topology in NuPRL
by Francisco Mota, Mark Bickford
2014
Synthetic topology is a recent branch of topology which takes continuous functions as basic as well as a certain Sierpinski space, and derives notions of topology from these two primitives in accordance with their standard interpretation in classical topology. This interpretation of topology is constructive, and it is useful in analyzing the semantics of (functional) programming languages, and for doing computability theory.
We recently discovered that NuPRL is capable of expressing the Sierpinski space as a type, and thereby potentially capable of formalizing large swathes of this theory (without adding any continuity assumptions). This presentation will be about the Sierpinski type, its properties, what we have shown so far, what we believe can be shown, and about the currently known limitations of this approach.