Name
Abstract | ||
|---|---|---|
In this paper, we develop a library of typed proof search procedures, and demonstrate their remarkable utility as a mechanism for proof-search and automation. We describe a framework for describing proof-search procedures in Agda, with a library of tactical combinators based on applicative functors. This framework is very general, so we demonstrate the approach with two common applications from the field of software verification: a library for property-based testing in the style of SmallCheck, and the embedding of a basic model checker inside our framework, which we use to verify the correctness of common concurrency algorithms. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2976022.2976030 | TyDe@ICFP |
DocType | Citations | PageRank |
Conference | 1 | 0.36 |
References | Authors | |
10 | 1 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Liam O'Connor | 1 | 44 | 5.02 |