Toward SMT-Based Refinement Types in Agda

Gan Shen, Lindsey Kuper

Dependent types offer great versatility and power, but developing proofs with them can be tedious and requires considerable human guidance. We propose to integrate Satisfiability M…