Lambda the Ultimate

I'm in the middle of writing an Object-Pascal-to-Java translator. One interesting aspect is the mapping between source and target types. Is anybody aware of literature about this topic, books, papers, etc.?

I would be interested in things like rules for "widening" a target type over the source type; constraints that must hold on operations applied in the target language so that the result complies with the result in the source language; maybe a formalism where you could even show (prove) that, given some sets of types and operations; etc.

I do not aim to set things up this way, but would enjoy reading some theoretical material about what I'm doing. Is there serious research in the area of source translation, anyway?