Recursion Schemes, Collapsible Pushdown Automata and Higher-Order Model Checking
作者： Luke Ong
DOI: 10.1007/978-3-642-37064-9_3
关键词:
摘要: This paper is about two models of computation that underpin recent developments in the algorithmic verification higher-order computation. Recursion schemes are essence simply-typed lambda calculus with recursion, generated from first-order symbols. Collapsible pushdown automata a generalisation to stacks — which iterations stack contain symbols equipped links. We study and compare expressive power properties infinite structures such as trees graphs by them. conclude brief overview applications model checking functional programs. A central theme work fruitful interplay ideas between neighbouring fields semantics verification.
springer.com
ioc.ee 参考文章(75)
W. Damm, Higher type program schemes and their tree languages Theoretical Computer Science. pp. 51- 72 ,(1977) , 10.1007/3-540-08138-0_5
Maurice Nivat, Langages algébriques sur le magma libre et sémantique des schémas de programme. international colloquium on automata, languages and programming. pp. 293- 308 ,(1972)
Pierre-Louis Curien, Hugo Herbelin, Computing with Abstract Böhm Trees. international symposium on functional and logic programming. pp. 20- 39 ,(1998)
Andrzej Murawski, C-H Luke Ong, Igor Walukiewicz, Idealized Algol with Ground Recursion, and DPDA Equivalence Automata, Languages and Programming. ,vol. 3580, pp. 917- 929 ,(2005) , 10.1007/11523468_74
Bruno COURCELLE, Recursive applicative program schemes Handbook of theoretical computer science (vol. B). pp. 459- 492 ,(1991) , 10.1016/B978-0-444-88074-1.50014-7
Maurice Nivat, On the interpretation of recursive program schemes ,(1974) , 10.22028/D291-26058
Javier Esparza, Stefan Schwoon, A BDD-Based Model Checker for Recursive Programs computer aided verification. pp. 324- 336 ,(2001) , 10.1007/3-540-44585-4_30
Didier Caucal, On Infinite Transition Graphs Having a Decidable Monadic Theory international colloquium on automata languages and programming. pp. 194- 205 ,(1996) , 10.1007/3-540-61440-0_128
Pawel Parys, Collapse Operation Increases Expressive Power of Deterministic Higher Order Pushdown Automata symposium on theoretical aspects of computer science. ,vol. 9, pp. 603- 614 ,(2011) , 10.4230/LIPICS.STACS.2011.603
Klaus Aehlig, Jolie G. de Miranda, C. -H. Luke Ong, The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable international conference on typed lambda calculi and applications. pp. 39- 54 ,(2005) , 10.1007/11417170_5