Constructive Ackermann's interpretation (Q2120969)

In this very readable written article, the author offers a constructive version of Kaye and Wong's result that ZF\(^{fin}\), a finitary version of ZF, is bi-interpretable with PA [\textit{R. Kaye} and \textit{T. L. Wong}, Notre Dame J. Formal Logic 48, No. 4, 497--510 (2007; Zbl 1137.03019)] in the following form: Heyting arithmetic HA is bi-interpretable with finitary version of constructive set theory CZF\(^{fin}\).