Dear all, Does anyone know of mechanized operational semantics for constraint/logic programming languages? I am interested in mechanized semantic (in Agda/Coq/...) for anything from ML constraints, to CHR, to Prolog and friends. Thank you, Arjen Rouvoet