Skip to content

Research at St Andrews

Proof-carrying plans

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

Christopher Joseph Schwaab, Ekaterina Komendantskaya, Alisdair Hill, František Farka, Ronald Petrick, Joe Wells, Kevin Hammond

School/Research organisations

Abstract

It is becoming increasingly important to verify safety and security of AI applications. While declarative languages (of the kind found in automated planners and model checkers) are traditionally used for verifying AI systems, a big challenge is to design methods that generate verified executable programs. A good example of such a “verification to implementation” cycle is given by automated planning languages like PDDL, where plans are found via a model search in a declarative language, but then interpreted or compiled into executable code in an imperative language. In this paper, we show that this method can itself be verified. We present a formal framework and a prototype Agda implementation that represent PDDL plans as executable functions that inhabit types that are given by formulae describing planning problems. By exploiting the well-known Curry-Howard correspondence, type-checking then automatically ensures that the generated program corresponds precisely to the specification of the planning problem.
Close

Details

Original languageEnglish
Title of host publicationPractical Aspects of Declarative Languages
Subtitle of host publication21st International Symposium, PADL 2019, Lisbon, Portugal, January 14-15, 2019, Proceedings
EditorsJose Julio Alferes, Moa Johansson
Place of PublicationCham
PublisherSpringer
Pages204-220
Number of pages19
ISBN (Print)9783030059972
DOIs
Publication statusPublished - Jan 2019
Event21st International Symposium on Practical Aspects of Declarative Languages (PADL 2019) - Lisbon, Portugal
Duration: 14 Jan 201915 Jan 2019
Conference number: 21
https://popl19.sigplan.org/track/PADL-2019#About

Publication series

NameLecture Notes in Computer Science (Programming and Software Engineering)
PublisherSpringer
Volume11372
ISSN (Print)0302-9743

Conference

Conference21st International Symposium on Practical Aspects of Declarative Languages (PADL 2019)
Abbreviated titlePADL 2019
CountryPortugal
CityLisbon
Period14/01/1915/01/19
Internet address

    Research areas

  • API planning, Curry-Howard correspondence, Constructive logic, Verification, Dependent types

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

ID: 256607242