Total Parser Combinators in Agda
The motivation and design decisions behind agdarsec are detailed in:
To typecheck and compile this project you will need:
I have ported this library to other dependently-typed languages: