Analysing the complexity of functional programs: higher-order meets first-order, ICFP'15, pp.152-164, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01231809
Term Rewriting and All That 9 More precisely, completion may add some epsilon transitions in this set of transitions, but the syntactical equality test can be replaced by a test modulo epsilon transition closure, 1998. ,
Over-approximating descendants by synchronized tree languages, RTA'13 Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.128-142, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00808871
HANDLING NON LEFT-LINEAR RULES WHEN COMPLETING TREE AUTOMATA, International Journal of Foundations of Computer Science, vol.70, issue.05, 2009. ,
DOI : 10.1016/j.entcs.2004.07.017
URL : https://hal.archives-ouvertes.fr/hal-00561373
C-shore: a collapsible approach to higher-order verification, ICFP'13, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00865155
Polymorphic functions with set-theoretic types, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, 2014. ,
DOI : 10.1145/2535838.2535840
URL : https://hal.archives-ouvertes.fr/hal-00907166
A faithful encoding of programmable strategies into term rewriting systems, RTA'15 Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.74-88, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01119941
Sequentiality, Monadic Second-Order Logic and Tree Automata, Information and Computation, vol.157, issue.1-2, pp.25-51, 2000. ,
DOI : 10.1006/inco.1999.2838
URL : http://doi.org/10.1006/inco.1999.2838
How to characterize the language of ground normal forms, 1987. ,
URL : https://hal.archives-ouvertes.fr/inria-00075877
Reachability Analysis over Term Rewriting Systems, Journal of Automated Reasoning, vol.37, issue.1?2, pp.3-4341, 2004. ,
DOI : 10.1007/s10817-004-6246-0
URL : https://hal.archives-ouvertes.fr/inria-00071609
Closure of Tree Automata Languages under Innermost Rewriting, WRS'08, pp.23-38, 2008. ,
DOI : 10.1016/j.entcs.2009.03.033
URL : https://hal.archives-ouvertes.fr/inria-00578966
Decidable approximations of sets of descendants and sets of normal forms, RTA'98, pp.151-165, 1998. ,
DOI : 10.1007/BFb0052368
URL : https://hal.archives-ouvertes.fr/inria-00073364
A note on the Precision of the Tree Automata Completion ,
URL : https://hal.archives-ouvertes.fr/hal-01091393
Towards Static Analysis of Functional Programs Using Tree Automata Completion, WRLA'14, 2014. ,
DOI : 10.1007/978-3-319-12904-4_8
URL : https://hal.archives-ouvertes.fr/hal-00921814
Termination criteria for tree automata completion, Journal of Logical and Algebraic Methods in Programming, vol.85, issue.1, pp.3-33, 2016. ,
DOI : 10.1016/j.jlamp.2015.05.003
URL : https://hal.archives-ouvertes.fr/hal-01194533
Reachability Analysis and Tree Automata Calculations. IRISA / Université de Rennes 1 ,
Equational approximations for tree automata completion, Journal of Symbolic Computation, vol.45, issue.5, pp.574-597, 2010. ,
DOI : 10.1016/j.jsc.2010.01.009
URL : https://hal.archives-ouvertes.fr/inria-00495405
Tree Automata Completion for Static Analysis of Functional Programs ,
URL : https://hal.archives-ouvertes.fr/hal-00780124
Reachability Analysis of Innermost Rewriting, RTA'15 ,
URL : https://hal.archives-ouvertes.fr/hal-00848260
On tree automata that certify termination of left-linear term rewriting systems, RTA'05, pp.353-367, 2005. ,
Proving Termination of Programs Automatically with AProVE, IJCAR'14, pp.184-191, 2014. ,
DOI : 10.1007/978-3-319-08587-6_13
Mechanizing and Improving Dependency Pairs, Journal of Automated Reasoning, vol.34, issue.2, pp.155-203, 2006. ,
DOI : 10.1007/s10817-006-9057-7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.302
Flow analysis of lazy higher-order functional programs, Theoretical Computer Science, vol.375, issue.1-3, pp.120-136, 2007. ,
DOI : 10.1016/j.tcs.2006.12.030
Model Checking Higher-Order Programs, Journal of the ACM, vol.60, issue.3, p.2013 ,
DOI : 10.1145/2487241.2487246
Model-Checking Higher-Order Programs with Recursive Types, ESOP'13, pp.431-450, 2013. ,
DOI : 10.1007/978-3-642-37036-6_24
Higher-order multi-parameter tree transducers and recursion schemes for program verification, POPL'10, pp.495-508, 2010. ,
DOI : 10.1145/1706299.1706355
Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars, RTA'11 of LIPIcs. Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, 2011. ,
Finite Models vs Tree Automata in Safety Verification, RTA'12, pp.225-239, 2012. ,
Approximations for Strategies and Termination, Electronic Notes in Theoretical Computer Science, vol.70, issue.6, pp.1-20, 2002. ,
DOI : 10.1016/S1571-0661(04)80598-X
URL : http://doi.org/10.1016/s1571-0661(04)80598-x
Verifying higher-order functional programs with pattern-matching algebraic data types, POPL'11, 2011. ,
DOI : 10.1145/1925844.1926453
Regular Sets of Descendants for Constructor-Based Rewrite Systems, Proc. of LPAR'99, volume 1705 of LNAI, 1999. ,
DOI : 10.1007/3-540-48242-3_10
Regular Sets of Descendants by Some Rewrite Strategies, RTA'02, 2002. ,
DOI : 10.1007/3-540-45610-4_10
Automatic computation of data set definitions, Information Processing, vol.68, pp.456-461, 1969. ,
A Verification Technique Using Term Rewriting Systems and Abstract Interpretation, RTA'04, pp.119-133, 2004. ,
DOI : 10.1007/978-3-540-25979-4_9
Right-Linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability, RTA'11, 2000. ,
DOI : 10.1007/10721975_17
Abstract Refinement Types This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a copy of this license, ESOP'13 Creative Commons, 171 Second St, 2013. ,