Skip to Main content Skip to Navigation
Reports

Regular Language Type Inference with Term Rewriting - extended version

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 metadatas

Cited literature [37 references]  Display  Hide  Download

https://hal.inria.fr/hal-02795484
Contributor : Thomas Genet <>
Submitted on : Tuesday, June 9, 2020 - 3:53:29 PM
Last modification on : Saturday, July 11, 2020 - 3:14:59 AM

Identifiers

  • HAL Id : hal-02795484, version 1

Citation

Thomas Haudebourg, Thomas Genet, Thomas Jensen. Regular Language Type Inference with Term Rewriting - extended version. [Research Report] Inria. 2020. ⟨hal-02795484⟩

Share

Metrics

Record views

54

Files downloads

250