First-order lax logic : a framework for abstraction, constraints and refinement. - Matthew Walton (1998)