Regular Language Type Inference with Term Rewriting - extended version

Timothée Haudebourg (1) , Thomas Genet (1) , Thomas Jensen (1)

1 CELTIQUE - Software certification with semantic analysis

This paper defines a new type system applied to the fully automatic verification of safety properties of tree-processing higher order functional programs. We use term rewriting systems to model the program and its semantics and tree automata to model algebraic data types. We define the regular abstract interpretation of the input term rewriting system where the abstract domain is a set of regular languages. From the regular abstract interpretation we derive a type system where each type is a regular language. We define an inference procedure for this type system which allows us check the validity of safety properties. The inference mechanism is built on an invariant learning procedure based on the tree automata completion algorithm. This invariant learning procedure is regularly-complete and complete in refutation, meaning that if it is possible to give a regular type to a term then we will eventually find it, and if there is no possible type (regular or not) then we will eventually find a counterexample .

Domaines: Génie logiciel [cs.SE]; Informatique et langage [cs.CL]; Théorie et langage formel [cs.FL]

Timothée Haudebourg, Thomas Genet, Thomas Jensen. Regular Language Type Inference with Term Rewriting - extended version. Proceedings of the ACM on Programming Languages, 2020, International Conference on Functional Programming (ICFP), 4 (ICFP), pp.1-29. ⟨10.1145/3408994⟩. ⟨hal-02795484⟩