This is my bachelor degree project.
The demo folder is a single regualr expression package implemented with sml based on Robert Harper's Algorithm.
The project folder include the formal proof of Harper's algorithm with Coq
Anyway,this project is too simple, and I am sincerely hope any advice