A Lambda calculus for invertible (r-Turing computable) functions
I am not very familiar with the area, but there is some recent work from the programming languages community that might interest you, based on the idea of restricting to a language of type isomorphisms.  In particular, you could have a look at


Fractional Types by Roshan P. James, Zachary Sparks, Jacques Carette, and Amr Sabry


as well as various related publications which you can find on Amr Sabry's website.