Abstract: | In [W. Burr, Functional interpretation of Aczel's constructive set theory, Annals of Pure and Applied Logic 104 (2000) 31–73] Wolfgang Burr presents a functional interpretation of constructive set theory in all finite types, , in a theory of constructive set functionals. is a subtheory of , containing bounded quantifiers only. His interpretation theorem reduces the consistency problem of (and certain extensions thereof) to the consistency problem of .We want to study admissible rules in , i.e. rules under which is closed. To do so, we study a Troelstra-style q-hybrid of, in fact, a modification × of Burr's translation. We introduce this modification in order to close a minor gap in Burr's proof of the functional interpretation of the schema of (Strong Collection).First of all, but surely after a short introduction, we analyse the less complex translation of modified realisation mr and its hybrids mq and mrt. |