A formal framework for compositional compilation