一句话：提出以正则语言为类型的类型系统及推断，用项重写与树自动机自动验证树处理高阶函数程序的安全性质。
本文面向树处理的高阶函数式程序，目标是全自动验证其安全性质。作者用项重写系统建模程序及其语义，用树自动机建模代数数据类型；构造输入项重写系统的正则抽象解释，其抽象域为正则语言集合。由此导出一种类型系统，其中每个类型都是正则语言，并给出类型推断过程。推断机制基于树自动机补全算法的不变式学习，用于检查安全性质是否有效。该学习过程具有正则完备性与反驳完备性：若某词项能被赋予正则类型，最终会找到该类型；若不存在任何类型（正则或非正则），最终会找到反例。
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 counter-example.
@article{HaudebourgGJ20,
title = {Regular language type inference with term rewriting},
author = {Timothée Haudebourg and Thomas Genet and Thomas Jensen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3408994}
}