2026-07-26T01:20:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4360 2024-03-06T10:34:57Z ddc:004 open_access

Model Checking and Functional Program Transformations Haddad, Axel Higher-order recursion schemes Model checking Tree automata We study a model for recursive functional programs called higher order recursion schemes (HORS). We give new proofs of two verification related problems: reflection and selection for HORS. The previous proofs are based on the equivalence between HORS and collapsible pushdown automata and they lose the structure of the initial program. The constructions presented here are based on shape preserving transformations, and can be applied on actual programs without losing the structure of the program. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Axel Haddad 2013 Is Part Of LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2013.115 urn:nbn:de:0030-drops-43605 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.115 eng https://creativecommons.org/licenses/by/3.0/legalcode