Liquid Types

@inproceedings{rondon:lt, abstract = {We present Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without paying the heavy price of of manual annotation. We have implemented liquid type inference in Dsolve, which takes as input an Ocaml program and a set of logical qualifiers and infers dependent types for the expressions in the Ocaml program. To demonstrate the utility of our approach, we describe experiments using Dsolve to statically verify the safety of array accesses on a set of Ocaml benchmarks that were previously annotated with dependent types as part of the DML project. We show that when used in conjunction with a simple set of bounds checking qualifiers, Dsolve reduces the amount of manual annotation required for proving safety from 31\% of program text to under 1\%.}, author = {Rondon, Patrick and Kawaguchi, Ming and Jhala, Ranjit }, booktitle = {Proceedings of the 30th ACM Conference on Programming Language Design and Implementation}, citeulike-article-id = {2910057}, keywords = {dependent-types, functional-programming, ocaml, type-theory}, posted-at = {2008-06-20 11:30:13}, priority = {0}, title = {Liquid Types}, url = {http://pho.ucsd.edu/liquid/}, year = {2008} }

TY - CONF ID - rondon:lt L3 - citeulike-article-id:2910057 TI - Liquid Types T2 - Proceedings of the 30th ACM Conference on Programming Language Design and Implementation N2 - We present Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without paying the heavy price of of manual annotation. We have implemented liquid type inference in Dsolve, which takes as input an Ocaml program and a set of logical qualifiers and infers dependent types for the expressions in the Ocaml program. To demonstrate the utility of our approach, we describe experiments using Dsolve to statically verify the safety of array accesses on a set of Ocaml benchmarks that were previously annotated with dependent types as part of the DML project. We show that when used in conjunction with a simple set of bounds checking qualifiers, Dsolve reduces the amount of manual annotation required for proving safety from 31% of program text to under 1%. KW - dependent-types KW - functional-programming KW - ocaml KW - type-theory AU - Rondon, Patrick AU - Kawaguchi, Ming AU - Jhala, Ranjit PY - 2008/// UR - http://pho.ucsd.edu/liquid/ ER -