Verifying Program Invariants with Refinement Types Frank Pfenning Carnegie Mellon University http://www.cs.cmu.edu/~fp/ fp@cs.cmu.edu In current programming languages there is a large gap between the minimal consistency guaranteed by type-checking and total correctness of a program, which generally cannot be established in practice. We present a system of refinement types which stops far short of full verification, but which allows many relevant and interesting program invariants to be formally expressed and verified. We illustrate why such a system requires both subtyping and intersection types, and investigate how these constructs interact with other language features such as exceptions and effects. Our concrete realization will be as an extension of ML, but the underlying design is quite robust and has been applied to other languages such as logical frameworks. While full inference of refinement types is decidable and principal types exist, it is neither feasible nor desirable in practice. We discuss why and present our current design for partial type reconstruction and its interaction with a module system. [Joint work with Rowan Davies]