# Actions You Can Handle: Dependent Types for AI Plans

arXiv: https://arxiv.org/abs/2105.11267 · HTML: https://mlsanity.com/paper/2105.11267/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 36 references that are in the map.
- First posted on arXiv 24 May 2021.

## Builds on (most cited first, 4 of 4)

- [Towards Explainable AI Planning as a Service](https://mlsanity.com/paper/1908.05059/) (2019)
- [Computing Plan-Length Bounds Using Lengths of Longest Paths](https://mlsanity.com/paper/2006.01011/) (2020)
- [Proof Relevant Corecursive Resolution](https://mlsanity.com/paper/1511.09394/) (2015)
- [Proof-Carrying Plans: a Resource Logic for AI Planning](https://mlsanity.com/paper/2008.04165/) (2020)

## Abstract (arXiv)

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.