Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
By Marie Kerjean
Creative telescoping for D-finite functions - Lecture 1
By Christoph Koutschan
By Thomas Genet
Appears in collection : Frontiers of reconnaissability / Frontières de la reconnaissabilité
Tree Automata Completion is an algorithm computing, or approximating, terms reachable by a term rewriting system. For many classes of term rewriting systems whose set of reachable terms is known to be regular, this algorithm is exact. Besides, the same algorithm can handle ²²any²² left-linear term rewriting system, in an approximated way, using equational 2 abstractions. Thanks to those two properties, we will see that regular languages and tree automata completion provide a promising alternative for automatic static analysis of functional programs.