Mechanizing Refinement Types

indebted to Ranjit for taking me on as his student when I was a complete beginner at type theory and software verification research. He provided the original motivation for my work in his 2019 graduate class on LIQUIDHASKELL, and I've been hooked on theorem proving ever since. I appreciate Ranjit's insights and feedback during our meetings and, most of all, his continuing confidence in my work throughout four conference rejections motivated me to keep improving and adding to our work. I would also like to thank my collaborator and coauthor Niki Vazou for all of her patient help, support, and ideas. I couldn't have done this research without her support either! I want to thank each of the members of my committee, Nadia Polikarpova, Victor Vianu, Sam Buss, and Cormac Flanagan for their support through this process and for the opportunity to TA for some of their classes as well. I want to thank my wife Ashley and our sons Kiyoshi, Daikichi, and Zygmunt for their patience and support for the many hours that I spent away from them working on the mechanizations and on this dissertation. I want to thank my fellow PL students for many helpful conversations, and especially Saketh Kasibatla, Kyle Thompson, and Cole Kurashige for helpful conversations about COQ and theorem proving. I also thank James Parker for a helpful discussion about data propositions and the anonymous reviewers across five conferences for their useful comments and suggestions. I owe a debt of gratitude to Joe Politz and Sorin Lerner for detailed comments and feedback on an early version of my POPL 24 talk. ix Work adapted in this dissertation Chapters 1-3, 5-8, and the conclusion are adapted from "Mechanizing Refinement Types" in the proceedings of the 51 st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024), by Michael Borkowski, Niki Vazou, and Ranjit Jhala. Chapter 4 is adapted from unpublished material that was originally prepared for the same "Mechanizing Refinement Types" by Michael Borkowski, Niki Vazou, and Ranjit Jhala but did not appear in the final published version.

Chapter 9 describes unpublished work done in collaboration with Ranjit Jhala.