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}
}