Strong functional pearl: Harper’s regular-expression matcher in Cedille
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Aug 02, 2020
- Source ID
- 10.1145/3409004
Entities
People
- Aaron Stump
- Christa Jenkins
- Colin Mcdonald
- Stephan Spahn
Organizations
- National Science Foundation
- United States Department of Defense
- University of Iowa
- University of Notre Dame