一句话：在 Cedille 中用递归宇宙接口将 Harper 的续延式正则表达式匹配器实现为强函数式程序，静态保证其全输入终止。
本文回应 Bove、Krauss 和 Sozeau 提出的挑战，在 Cedille 中将 Harper 基于续延的正则表达式匹配器实现为强函数式程序。其关键不是依赖类型或显式终止证明，而是使用 Cedille 提供的“递归宇宙”接口：语言保证所有针对该接口编写的程序都终止，而程序员只需用标准多态类型检查代码是否符合接口。该实现展示了无需复杂类型机制即可获得全输入终止保证的强函数式编程风格，并为以正则匹配器为代表的非结构化递归程序提供了可静态验证的终止方案。
This paper describes an implementation of Harper's continuation-based regular-expression matcher as a strong functional program in Cedille; i.e., Cedille statically confirms termination of the program on all inputs. The approach uses neither dependent types nor termination proofs. Instead, a particular interface dubbed a recursion universe is provided by Cedille, and the language ensures that all programs written against this interface terminate. Standard polymorphic typing is all that is needed to check the code against the interface. This answers a challenge posed by Bove, Krauss, and Sozeau.
@article{StumpJSM20,
title = {Strong functional pearl: Harper’s regular-expression matcher in Cedille},
author = {Aaron Stump and Christopher Jenkins and Stephan Spahn and Colin McDonald},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3409004}
}