- Porting to ghc-8
  - restore benchmarks
  - look at Target's model

- Gradual Refinement Types
 - [ ] clean up code
 - [ ] restore old structures
 - [ ] pull request 
 - [ ] print readable solutions 
 - [ ] Implement Eric's validity with measures 
 - [x] Check how elimination interacts with graduals (eg Interpretation fails with elimination now)
 - [ ] Find interesting application
 - [ ] Present weakest result 


- Proof by Symbolic Evaluation