Revisiting Soundness for Occurrence Typing, Semantically

Yuquan Fu, Carlo Angiuli, Sam Tobin-Hochstadt

Over the past two decades, numerous systems have brought some of the benefits of dependent typing to a wide variety of new programming languages, often by restricting which terms c…