Proof-carrying plans

Christopher Schwaab, Ekaterina Komendantskaya, Alasdair Hill, František Farka, Ronald P. A. Petrick, Joe Wells, Kevin Hammond

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

4 Citations (Scopus)
45 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationPractical Aspects of Declarative Languages
Subtitle of host publicationPADL 2019
EditorsJosé Júlio Alferes, Moa Johansson
Number of pages17
ISBN (Electronic)9783030059989
ISBN (Print)9783030059972
Publication statusPublished - 2019
Event20th International Symposium on Practical Aspects of Declarative Languages 2018 - Los Angeles, United States
Duration: 8 Jan 20189 Jan 2018

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference20th International Symposium on Practical Aspects of Declarative Languages 2018
Abbreviated titlePADL 2018
Country/TerritoryUnited States
CityLos Angeles


  • AI planning
  • Constructive logic
  • Curry-Howard correspondence
  • Dependent types
  • Verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Proof-carrying plans'. Together they form a unique fingerprint.

Cite this