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.