Certifying algorithms and relevant properties of Reversible Primitive Permutations with Lean G Maletto, L Roversi - arXiv preprint arXiv:2201.10443, 2022 - arxiv.org Reversible Primitive Permutations (RPP) are recursively defined functions designed to model Reversible Computation. We illustrate a proof, fully developed with the proof-assistant Lean, certifying that:" RPP can encode every Primitive Recursive Function". Our reworking of …