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 be...
Main Authors: | , , |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Published: |
2008
|
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.165.65 http://www.cs.ucsd.edu/~prondon/papers/liquid-types-pldi08.pdf |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.165.65 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.165.65 2023-05-15T16:01:56+02:00 Liquid types Patrick M. Rondon Ming W. Kawaguchi Ranjit Jhala The Pennsylvania State University CiteSeerX Archives 2008 application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.165.65 http://www.cs.ucsd.edu/~prondon/papers/liquid-types-pldi08.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.165.65 http://www.cs.ucsd.edu/~prondon/papers/liquid-types-pldi08.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.cs.ucsd.edu/~prondon/papers/liquid-types-pldi08.pdf General Terms Languages Reliability Verification Keywords Dependent Types Hindley-Milner Predicate Abstraction Type Inference text 2008 ftciteseerx 2016-01-07T15:51:26Z 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%. Text DML Unknown |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
ftciteseerx |
language |
English |
topic |
General Terms Languages Reliability Verification Keywords Dependent Types Hindley-Milner Predicate Abstraction Type Inference |
spellingShingle |
General Terms Languages Reliability Verification Keywords Dependent Types Hindley-Milner Predicate Abstraction Type Inference Patrick M. Rondon Ming W. Kawaguchi Ranjit Jhala Liquid types |
topic_facet |
General Terms Languages Reliability Verification Keywords Dependent Types Hindley-Milner Predicate Abstraction Type Inference |
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%. |
author2 |
The Pennsylvania State University CiteSeerX Archives |
format |
Text |
author |
Patrick M. Rondon Ming W. Kawaguchi Ranjit Jhala |
author_facet |
Patrick M. Rondon Ming W. Kawaguchi Ranjit Jhala |
author_sort |
Patrick M. Rondon |
title |
Liquid types |
title_short |
Liquid types |
title_full |
Liquid types |
title_fullStr |
Liquid types |
title_full_unstemmed |
Liquid types |
title_sort |
liquid types |
publishDate |
2008 |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.165.65 http://www.cs.ucsd.edu/~prondon/papers/liquid-types-pldi08.pdf |
genre |
DML |
genre_facet |
DML |
op_source |
http://www.cs.ucsd.edu/~prondon/papers/liquid-types-pldi08.pdf |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.165.65 http://www.cs.ucsd.edu/~prondon/papers/liquid-types-pldi08.pdf |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766397607312097280 |