Journal article
Strong functional pearl: Harper’s regular-expression matcher in Cedille
Proceedings of ACM on programming languages, Vol.4(ICFP), pp.1-25
08/02/2020
DOI: 10.1145/3409004
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.
Details
- Title: Subtitle
- Strong functional pearl: Harper’s regular-expression matcher in Cedille
- Creators
- Aaron Stump - University of IowaChristopher Jenkins - University of IowaStephan Spahn - University of IowaColin McDonald - University of Notre Dame
- Resource Type
- Journal article
- Publication Details
- Proceedings of ACM on programming languages, Vol.4(ICFP), pp.1-25
- DOI
- 10.1145/3409004
- ISSN
- 2475-1421
- eISSN
- 2475-1421
- Grant note
- DOI: 10.13039/501100001809, name: National Science Foundation, award: 1524519; DOI: 10.13039/100000005, name: U.S. Department of Defense, award: FA9550-16-1-0082
- Language
- English
- Date published
- 08/02/2020
- Academic Unit
- Computer Science
- Record Identifier
- 9984259491102771
Metrics
12 Record Views