TyDe '21: "Actions You Can Handle: Dependent ..."
Actions You Can Handle: Dependent Types for AI Plans
Alasdair Hill, Ekaterina Komendantskaya, Matthew L. Daggitt, and Ronald P. A. Petrick
(Heriot-Watt University, UK)
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 the 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.
@InProceedings{TyDe21p1,
author = {Alasdair Hill and Ekaterina Komendantskaya and Matthew L. Daggitt and Ronald P. A. Petrick},
title = {Actions You Can Handle: Dependent Types for AI Plans},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3471875.3472990},
year = {2021},
}
Publisher's Version
Info
TyDe '21: "Actions You Can Handle: Dependent ..."
Actions You Can Handle: Dependent Types for AI Plans
Alasdair Hill, Ekaterina Komendantskaya, Matthew L. Daggitt, and Ronald P. A. Petrick
(Heriot-Watt University, UK)
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 the 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.
@InProceedings{TyDe21p1,
author = {Alasdair Hill and Ekaterina Komendantskaya and Matthew L. Daggitt and Ronald P. A. Petrick},
title = {Actions You Can Handle: Dependent Types for AI Plans},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3471875.3472990},
year = {2021},
}
Publisher's Version
Info
TyDe '21: "Actions You Can Handle: Dependent ..."
Actions You Can Handle: Dependent Types for AI Plans
Alasdair Hill, Ekaterina Komendantskaya, Matthew L. Daggitt, and Ronald P. A. Petrick
(Heriot-Watt University, UK)
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 the 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.
@InProceedings{TyDe21p1,
author = {Alasdair Hill and Ekaterina Komendantskaya and Matthew L. Daggitt and Ronald P. A. Petrick},
title = {Actions You Can Handle: Dependent Types for AI Plans},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3471875.3472990},
year = {2021},
}
Publisher's Version
Info
TyDe '21: "Actions You Can Handle: Dependent ..."
Actions You Can Handle: Dependent Types for AI Plans
Alasdair Hill, Ekaterina Komendantskaya, Matthew L. Daggitt, and Ronald P. A. Petrick
(Heriot-Watt University, UK)
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 the 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.
@InProceedings{TyDe21p1,
author = {Alasdair Hill and Ekaterina Komendantskaya and Matthew L. Daggitt and Ronald P. A. Petrick},
title = {Actions You Can Handle: Dependent Types for AI Plans},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3471875.3472990},
year = {2021},
}
Publisher's Version
Info
TyDe '21: "A Simpler Encoding of Indexed ..."
A Simpler Encoding of Indexed Types
Yinsen Zhang
(Pennsylvania State University, USA)
In functional programming languages, generalized algebraic data types (GADTs) are very useful as the unnecessary pattern matching over them can be ruled out by the failure of unification of type arguments. In dependent type systems, this is usually called indexed types and it’s particularly useful as the identity type is a special case of it. However, pattern matching over indexed types is very complicated as it requires term unification in general. We study a simplified version of indexed types (called simpler indexed types) where we explicitly specify the selection process of constructors, and we discuss its expressiveness, limitations, and properties.
@InProceedings{TyDe21p14,
author = {Yinsen Zhang},
title = {A Simpler Encoding of Indexed Types},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {14--22},
doi = {10.1145/3471875.3472991},
year = {2021},
}
Publisher's Version