Proof-carrying plans

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

doi:10.1007/978-3-030-05998-9_13

Proof-carrying plans

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Practical Aspects of Declarative Languages
Subtitle of host publication	21st International Symposium, PADL 2019, Lisbon, Portugal, January 14-15, 2019, Proceedings
Editors	Jose Julio Alferes, Moa Johansson
Place of Publication	Cham
Publisher	Springer
Pages	204-220
Number of pages	19
ISBN (Print)	9783030059972
DOIs	https://doi.org/10.1007/978-3-030-05998-9_13
Publication status	Published - Jan 2019
Event	21st International Symposium on Practical Aspects of Declarative Languages (PADL 2019) - Lisbon, Portugal Duration: 14 Jan 2019 → 15 Jan 2019 Conference number: 21 https://popl19.sigplan.org/track/PADL-2019#About

Publication series

Name	Lecture Notes in Computer Science (Programming and Software Engineering)
Publisher	Springer
Volume	11372
ISSN (Print)	0302-9743

Conference

Conference	21st International Symposium on Practical Aspects of Declarative Languages (PADL 2019)
Abbreviated title	PADL 2019
Country/Territory	Portugal
City	Lisbon
Period	14/01/19 → 15/01/19
Internet address	https://popl19.sigplan.org/track/PADL-2019#About

Keywords

API planning
Curry-Howard correspondence
Constructive logic
Verification
Dependent types

Access to Document

10.1007/978-3-030-05998-9_13

padl-pddl-verification
© 2019, Springer Nature Switzerland AG. This work has been made available online in accordance with the publisher's policies. This is the author created accepted version manuscript following peer review and as such may differ slightly from the final published version. The final published version of this work is available at https://doi.org/10.1007/978-3-030-05998-9_13
Accepted author manuscript, 116 KBLicence: Unspecified

TeamPlay: H2020 ICT-5 Teamplay
Brown, C. (PI)
European Commission
1/01/18 → 31/12/20
Project: Standard
Discovery: Pattern Discovery and Program: Discovery: Pattern Discovery and Program Shaping for Manycore Systems
Thomson, J. (PI), Hammond, K. (CoI) & Sarkar, S. (CoI)
EPSRC
1/07/17 → 31/12/20
Project: Standard

Cite this

Schwaab, C. J., Komendantskaya, E., Hill, A., Farka, F., Petrick, R., Wells, J., & Hammond, K. (2019). Proof-carrying plans. In J. J. Alferes, & M. Johansson (Eds.), Practical Aspects of Declarative Languages: 21st International Symposium, PADL 2019, Lisbon, Portugal, January 14-15, 2019, Proceedings (pp. 204-220). (Lecture Notes in Computer Science (Programming and Software Engineering); Vol. 11372). Springer. https://doi.org/10.1007/978-3-030-05998-9_13

Schwaab, Christopher Joseph ; Komendantskaya, Ekaterina ; Hill, Alisdair et al. / Proof-carrying plans. Practical Aspects of Declarative Languages: 21st International Symposium, PADL 2019, Lisbon, Portugal, January 14-15, 2019, Proceedings. editor / Jose Julio Alferes ; Moa Johansson. Cham : Springer, 2019. pp. 204-220 (Lecture Notes in Computer Science (Programming and Software Engineering)).

@inproceedings{cfd986883e2a4da7b702984d65624446,

title = "Proof-carrying plans",

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.",

keywords = "API planning, Curry-Howard correspondence, Constructive logic, Verification, Dependent types",

author = "Schwaab, {Christopher Joseph} and Ekaterina Komendantskaya and Alisdair Hill and Franti{\v s}ek Farka and Ronald Petrick and Joe Wells and Kevin Hammond",

year = "2019",

month = jan,

doi = "10.1007/978-3-030-05998-9_13",

language = "English",

isbn = "9783030059972",

series = "Lecture Notes in Computer Science (Programming and Software Engineering)",

publisher = "Springer",

pages = "204--220",

editor = "Alferes, {Jose Julio} and Moa Johansson",

booktitle = "Practical Aspects of Declarative Languages",

address = "Netherlands",

note = "21st International Symposium on Practical Aspects of Declarative Languages (PADL 2019), PADL 2019 ; Conference date: 14-01-2019 Through 15-01-2019",

url = "https://popl19.sigplan.org/track/PADL-2019#About",

}

Schwaab, CJ, Komendantskaya, E, Hill, A, Farka, F, Petrick, R, Wells, J & Hammond, K 2019, Proof-carrying plans. in JJ Alferes & M Johansson (eds), Practical Aspects of Declarative Languages: 21st International Symposium, PADL 2019, Lisbon, Portugal, January 14-15, 2019, Proceedings. Lecture Notes in Computer Science (Programming and Software Engineering), vol. 11372, Springer, Cham, pp. 204-220, 21st International Symposium on Practical Aspects of Declarative Languages (PADL 2019), Lisbon, Portugal, 14/01/19. https://doi.org/10.1007/978-3-030-05998-9_13

Proof-carrying plans. / Schwaab, Christopher Joseph; Komendantskaya, Ekaterina; Hill, Alisdair et al.
Practical Aspects of Declarative Languages: 21st International Symposium, PADL 2019, Lisbon, Portugal, January 14-15, 2019, Proceedings. ed. / Jose Julio Alferes; Moa Johansson. Cham: Springer, 2019. p. 204-220 (Lecture Notes in Computer Science (Programming and Software Engineering); Vol. 11372).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Proof-carrying plans

AU - Schwaab, Christopher Joseph

AU - Komendantskaya, Ekaterina

AU - Hill, Alisdair

AU - Farka, František

AU - Petrick, Ronald

AU - Wells, Joe

AU - Hammond, Kevin

N1 - Conference code: 21

PY - 2019/1

Y1 - 2019/1

N2 - 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.

AB - 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.

KW - API planning

KW - Curry-Howard correspondence

KW - Constructive logic

KW - Verification

KW - Dependent types

U2 - 10.1007/978-3-030-05998-9_13

DO - 10.1007/978-3-030-05998-9_13

M3 - Conference contribution

SN - 9783030059972

T3 - Lecture Notes in Computer Science (Programming and Software Engineering)

SP - 204

EP - 220

BT - Practical Aspects of Declarative Languages

A2 - Alferes, Jose Julio

A2 - Johansson, Moa

PB - Springer

CY - Cham

T2 - 21st International Symposium on Practical Aspects of Declarative Languages (PADL 2019)

Y2 - 14 January 2019 through 15 January 2019

ER -

Schwaab CJ, Komendantskaya E, Hill A, Farka F, Petrick R, Wells J et al. Proof-carrying plans. In Alferes JJ, Johansson M, editors, Practical Aspects of Declarative Languages: 21st International Symposium, PADL 2019, Lisbon, Portugal, January 14-15, 2019, Proceedings. Cham: Springer. 2019. p. 204-220. (Lecture Notes in Computer Science (Programming and Software Engineering)). Epub 2018 Dec 19. doi: 10.1007/978-3-030-05998-9_13

Proof-carrying plans

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Projects

TeamPlay: H2020 ICT-5 Teamplay

Discovery: Pattern Discovery and Program: Discovery: Pattern Discovery and Program Shaping for Manycore Systems

Cite this