Structural refinement types

authors: David Binder, Ingo Skupin, David Läwen, Klaus Ostermann
year: 2022
url: https://dl.acm.org/doi/abs/10.1145/3546196.3550163
publisher: ACM
abstract: Static types are a great form of lightweight static analysis. But sometimes a type like List is too coarse – we would also like to work with its refinements like non-empty lists, or lists containing exactly 42 elements. Dependent types allow for this, but they impose a heavy proof burden on the programmer. We want the checking and inference of refinements to be fully automatic.