With Iztok Kavkler.
Abstract: RZ is a tool which translates axiomatizations of mathematical structures to program speciļ¬cations using the realizability interpretation of logic. This helps programmers correctly implement data structures for computable mathematics. RZ does not prescribe a particular method of implementation, but allows programmers to write efficient code by hand, or to extract trusted code [...]