@inproceedings{bdaf8fd4df2d437caaa6d774c6bed3f3,
title = "Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection",
abstract = "Higher-order recursion schemes are rewriting systems for simply typed terms and they are known to be equi-expressive with collapsible pushdown automata (CPDA) for generating trees. We argue that CPDA are an essential model when working with recursion schemes. First, we give a new proof of the translation of schemes into CPDA that does not appeal to game semantics. Second, we show that this translation permits to revisit the safety constraint and allows CPDA to be seen as Krivine machines. Finally, we show that CPDA permit one to prove the effective MSO selection property for schemes, subsuming all known decidability results for MSO on schemes.",
keywords = "Collapsible Pushdown Automata, MSO Effective Selection, Recursion Schemes, Safety Constraint",
author = "Arnaud Carayol and Olivier Serre",
year = "2012",
month = oct,
day = "11",
doi = "10.1109/LICS.2012.73",
language = "English",
isbn = "9780769547695",
series = "Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012",
pages = "165--174",
booktitle = "Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012",
note = "2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012 ; Conference date: 25-06-2012 Through 28-06-2012",
}