  Verification of AI is a challenge that has engineering, algorithmic and
programming language components. For example, AI planners are deployed to model
actions of autonomous agents. They comprise a number of searching algorithms
that, given a set of specified properties, find a sequence of actions that
satisfy these properties. Although AI planners are mature tools from the
algorithmic and engineering points of view, they have limitations as
programming languages. Decidable and efficient automated search entails
restrictions on the syntax of the language, prohibiting use of higher-order
properties or recursion. This paper proposes a methodology for embedding plans
produced by AI planners into dependently-typed language Agda, which enables
users to reason about and verify more general and abstract properties of plans,
and also provides a more holistic programming language infrastructure for
modelling plan execution.
