This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
We present a system of refinement types for LF in the style of recent formulations where only canonical forms are well-typed. Both the usual LF rules and the rules for type refine...
Refinement types sharpen systems of simple and dependent types by offering expressive means to more precisely classify well-typed terms. We present a system of refinement types for...
We present Low-Level Liquid Types, a refinement type system for C based on Liquid Types. Low-Level Liquid Types combine refinement types with three key elements to automate verifi...
Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala