Extensible datasort refinements

authors: Jana Dunfield
year: 2017
url: http://dx.doi.org/10.1007/978-3-662-54434-1₁8
publisher: Springer Berlin Heidelberg
abstract: Refinement types turn typechecking into lightweight verification. The classic form of refinement type is the datasort refinement, in which datasorts identify subclasses of inductive datatypes.