GLOW2018-formalization