Toward SMT-Based Refinement Types in Agda
Programming Languages
2021-10-13 v1
Abstract
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 Modulo Theories (SMT)-based refinement types into the dependently-typed language Agda in an effort to ease some of the burden of programming with dependent types and combine the strengths of the two approaches to mechanized theorem proving.
Cite
@article{arxiv.2110.05771,
title = {Toward SMT-Based Refinement Types in Agda},
author = {Gan Shen and Lindsey Kuper},
journal= {arXiv preprint arXiv:2110.05771},
year = {2021}
}
Comments
Accepted for publication at HATRA 2021