ICFP 2021
Sun 22 - Sat 28 August 2021
Mon 23 Aug 2021 01:30 - 02:00 at TyDe - Session III Chair(s): Dominic Orchard

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.

Mon 23 Aug

Displayed time zone: Seoul change

01:30 - 03:00
Session IIITyDe at TyDe
Chair(s): Dominic Orchard University of Kent, UK
Actions You Can Handle: Dependent Types for AI Plans
Alasdair Hill Heriot-Watt University, Ekaterina Komendantskaya Heriot-Watt University, UK, Matthew L. Daggitt Heriot-Watt University, Ronald P. A. Petrick Heriot-Watt University
DOI Pre-print Media Attached
Co-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
Uma Zalakain University of Glasgow, Ornela Dardha University of Glasgow
File Attached