I was doing some web searches to see if I could answer Todd Trimble’s questions here. As usual, instead of answers I found more papers to read and no time to read them.

On constructive set theory:

• Notes on Constructive Set Theory by Peter Aczel and Michael Rathjen. Aczel is the inventor of CZF, a constructive analogue of ZF.
• Programming in Martin-Löf’s Type Theory by Bengt Nordström, Kent Petersson, and Jan M. Smith. Martin-Löf’s Type Theory is apparently one of the few theories that is uncontroversially constructive.
• Predicative topos theory and models for constructive set theory by Benno van den Berg. This is a Ph.D. thesis that tries to weaken the notion of topos appropriately.

On realizability and the effective topos:

• Realizability: A Historical Essay by Jaap van Oosten.
• Categorical Models of Constructive Logic by Thomas Streicher.