A constructive version of the Lusin Separation Theorem

The Lusin Separation Theorem is one of the fundamental results of classical descriptive set theory. A version of the theorem has been proved by Wim Veldman in Intuitionistic mathematics. In my talk I will discuss a version provable in CZF (constructive Zermelo-Fraenkel set theory), which will yield as corollaries the original result in ZF+DC (ZF + axiom of dependent choice) and Veldman's result in CZF+BI_D (Bar Induction). The version provable in CZF is a `point-free' result somewhat in the style of Per Martin-Lof's 1970 book, 'Notes on Constructive Mathematics', which takes a point-free approach to Borel sets and the subset relation between them.