There is a tight fit between type theories à la Martin-Löf and constructive set theories such as Constructive Zermelo-Fraenkel set theory, CZF, and its extension as well as classical Kripke-Platek set theory and extensions thereof. The technology for determining their (exact) proof-theoretic strength was developed in the 1990s. The situation is rather different when it comes to type theories (with universes) having the impredicative type of propositions Prop from the Calculus of Constructions that features in some powerful proof assistants. Aczel's sets-as-types interpretation into these type theories gives rise to  rather unusual set-theoretic axioms: negative power set and negative separation. But it is not known how to determine the proof-theoretic strengths of intuitionistic set theories with such axioms via familiar classical set theories (though it is not difficult to see that ZFC plus infinitely many inaccessibles provides an upper bound). The first part of the talk will be a survey of known results from this area. The second part will be concerned with the rather special computational and proof-theoretic behavior of such theories.

Let G be a transitive permutation group. If G is finite, then a classical theorem of Jordan implies the existence of fixed-point-free elements, which we call derangements. This result has some interesting and unexpected applications, and it leads to several natural problems on the abundance and order of derangements that have been the focus of recent research. In this talk, I will discuss some of these related problems, and I will report on recent joint work with Hung Tong-Viet on primitive permutation groups with extremal derangement properties.