Refining semantics for multi-stage programming