search

totalscript / totalscript

Explore what a powerful type system can do.
Other
29 stars 3 forks source link

Automated Reasoning #3

Open rainoftime opened 7 years ago

rainoftime commented 7 years ago

How to integrate automatic reasoning tools?

Maybe we can learn from Isabelle/HOL?...

First-Order Theorem Proving

SAT & SMT

Computer Algebra System

Other:

rainoftime commented 7 years ago

需要z3 Idris binding之类的么（实验refinement type什么的...）？ @izgzhen ...

izgzhen commented 7 years ago

@rainoftime I guess you mean Z3 Haskell binding?...

izgzhen commented 7 years ago

@rainoftime not sure ... there are both Haskell & Idris in Idris impl