A New Refinement Type System for Automated nu-HFLZ Validity Checkin

on YouTube ↗25m

" summary

A refinement type system targets validity checking for a fragment of vHFLZ (no least fixpoints) and produces template-based constraints that are solved to decide safety properties of higher-order functional programs. An implementation, THFL solver, uses a more sophisticated subtyping relation than Burn et al.’s system, generates constraints reducible to CHCs when possible, and wins experimentally by solving more instances than Horus and often outperforming a CEGAR-based tool on benchmark suites. The system is sound, partially complete, and practical for many reductions from program safety.

AI-written summary · about

" chapters (13)

1. 0:00Introduction
2. 1:28Motivation for new checker
3. 2:10nu-HFLZ syntax overview
4. 3:12Greatest fixed points
5. 5:39Program verification with nu-HFLZ
6. 7:27Refinement type system design
7. 10:44RTy constraints importance
8. 13:36RTy assumptions efficiency
9. 15:03Comparison with prior work
10. 16:50Constraint solving algorithm
11. 20:45Experimental results
12. 22:32Conclusion and future work
13. 23:18Q&A