Liquid types
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...
Published in: | ACM SIGPLAN Notices |
---|---|
Main Authors: | , , |
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Association for Computing Machinery (ACM)
2008
|
Subjects: | |
Online Access: | http://dx.doi.org/10.1145/1379022.1375602 https://dl.acm.org/doi/pdf/10.1145/1379022.1375602 |
id |
cracm:10.1145/1379022.1375602 |
---|---|
record_format |
openpolar |
spelling |
cracm:10.1145/1379022.1375602 2024-09-15T18:03:52+00:00 Liquid types Rondon, Patrick M. Kawaguci, Ming Jhala, Ranjit 2008 http://dx.doi.org/10.1145/1379022.1375602 https://dl.acm.org/doi/pdf/10.1145/1379022.1375602 en eng Association for Computing Machinery (ACM) ACM SIGPLAN Notices volume 43, issue 6, page 159-169 ISSN 0362-1340 1558-1160 journal-article 2008 cracm https://doi.org/10.1145/1379022.1375602 2024-07-08T04:02:57Z 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 the heavy price 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 fixed set of array bounds checking qualifiers, DSOLVE reduces the amount of manual annotation required for proving safety from 31% of program text to under 1%. Article in Journal/Newspaper DML ACM Publications (Association for Computing Machinery) ACM SIGPLAN Notices 43 6 159 169 |
institution |
Open Polar |
collection |
ACM Publications (Association for Computing Machinery) |
op_collection_id |
cracm |
language |
English |
description |
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 the heavy price 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 fixed set of array bounds checking qualifiers, DSOLVE reduces the amount of manual annotation required for proving safety from 31% of program text to under 1%. |
format |
Article in Journal/Newspaper |
author |
Rondon, Patrick M. Kawaguci, Ming Jhala, Ranjit |
spellingShingle |
Rondon, Patrick M. Kawaguci, Ming Jhala, Ranjit Liquid types |
author_facet |
Rondon, Patrick M. Kawaguci, Ming Jhala, Ranjit |
author_sort |
Rondon, Patrick M. |
title |
Liquid types |
title_short |
Liquid types |
title_full |
Liquid types |
title_fullStr |
Liquid types |
title_full_unstemmed |
Liquid types |
title_sort |
liquid types |
publisher |
Association for Computing Machinery (ACM) |
publishDate |
2008 |
url |
http://dx.doi.org/10.1145/1379022.1375602 https://dl.acm.org/doi/pdf/10.1145/1379022.1375602 |
genre |
DML |
genre_facet |
DML |
op_source |
ACM SIGPLAN Notices volume 43, issue 6, page 159-169 ISSN 0362-1340 1558-1160 |
op_doi |
https://doi.org/10.1145/1379022.1375602 |
container_title |
ACM SIGPLAN Notices |
container_volume |
43 |
container_issue |
6 |
container_start_page |
159 |
op_container_end_page |
169 |
_version_ |
1810441316415307776 |