Пособие по реализации проверки для refinement-типов. В духе разработки компиляторов на основе техники nanopass. Предикаты проверяются с помощью SMT-решателя Z3.

Refinement Types: A Tutorial
https://arxiv.org/abs/2010.07763
https://github.com/ranjitjhala/sprite-lang

#analysis #smt