Unboundedness and downward closures of higher-order pushdown automata. / Hague, Matthew; Kochems, Jonathan; Ong, C.-H. Luke.

Principles of Programming Languages: POPL '16. New York, NY : ACM, 2016. p. 151-163.

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

Published

Standard

Unboundedness and downward closures of higher-order pushdown automata. / Hague, Matthew; Kochems, Jonathan; Ong, C.-H. Luke.

Principles of Programming Languages: POPL '16. New York, NY : ACM, 2016. p. 151-163.

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

Harvard

Hague, M, Kochems, J & Ong, C-HL 2016, Unboundedness and downward closures of higher-order pushdown automata. in Principles of Programming Languages: POPL '16. ACM, New York, NY, pp. 151-163. https://doi.org/10.1145/2837614.2837627

APA

Hague, M., Kochems, J., & Ong, C-H. L. (2016). Unboundedness and downward closures of higher-order pushdown automata. In Principles of Programming Languages: POPL '16 (pp. 151-163). ACM. https://doi.org/10.1145/2837614.2837627

Vancouver

Hague M, Kochems J, Ong C-HL. Unboundedness and downward closures of higher-order pushdown automata. In Principles of Programming Languages: POPL '16. New York, NY: ACM. 2016. p. 151-163 https://doi.org/10.1145/2837614.2837627

Author

Hague, Matthew ; Kochems, Jonathan ; Ong, C.-H. Luke. / Unboundedness and downward closures of higher-order pushdown automata. Principles of Programming Languages: POPL '16. New York, NY : ACM, 2016. pp. 151-163

BibTeX

@inproceedings{0f3c0b5d84cf4a15b7d54651138d34bd,
title = "Unboundedness and downward closures of higher-order pushdown automata",
abstract = "We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.",
keywords = "Higher-Order Programs, Functional Programs, Model-Checking, Verification, Formal Languages, Downward Closures, Parikh Images, Concurrency, Automata, Pushdown Automata",
author = "Matthew Hague and Jonathan Kochems and Ong, {C.-H. Luke}",
year = "2016",
month = jan,
day = "11",
doi = "10.1145/2837614.2837627",
language = "English",
isbn = "978-1-4503-3549-2",
pages = "151--163",
booktitle = "Principles of Programming Languages",
publisher = "ACM",

}

RIS

TY - GEN

T1 - Unboundedness and downward closures of higher-order pushdown automata

AU - Hague, Matthew

AU - Kochems, Jonathan

AU - Ong, C.-H. Luke

PY - 2016/1/11

Y1 - 2016/1/11

N2 - We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.

AB - We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.

KW - Higher-Order Programs

KW - Functional Programs

KW - Model-Checking

KW - Verification

KW - Formal Languages

KW - Downward Closures

KW - Parikh Images

KW - Concurrency

KW - Automata

KW - Pushdown Automata

U2 - 10.1145/2837614.2837627

DO - 10.1145/2837614.2837627

M3 - Conference contribution

SN - 978-1-4503-3549-2

SP - 151

EP - 163

BT - Principles of Programming Languages

PB - ACM

CY - New York, NY

ER -