Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
De Marie Kerjean
Creative telescoping for D-finite functions - Lecture 1
De Christoph Koutschan
De Thomas Genet
Apparaît dans la 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.