Mechanising a Modal Logic for Value-Passing Agents in HOL