Skip to Main content Skip to Navigation
Journal articles

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
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : 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 .
Complete list of metadata

Cited literature [37 references]  Display  Hide  Download
Contributor : Thomas Genet Connect in order to contact the contributor
Submitted on : Tuesday, June 9, 2020 - 3:53:29 PM
Last modification on : Friday, August 5, 2022 - 2:54:52 PM


Distributed under a Creative Commons Attribution 4.0 International License



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



Record views


Files downloads