Liquid Types, static verification: deduction, model checking, type systems | Hacker News Reader

Liquid Types, static verification: deduction, model checking, type systems

research.microsoft.com

79 pointsgtani14 comments

This kind of work should get much more attention than it does. It's non-trivial, fairly new and does something potentially very useful (which is more than I can say for most "X in JavaScripts" things submitted here).

http://goto.ucsd.edu/~pmr/papers/liquid-types-pldi08.pdf

Probably should have noted submitted URL is Silverlight video, or large download.

I don't understand enough to know how significant this work is. They present a system to infer dependent types, which, if it works well, would solve at least part of the problem of dependent types as I understand it: having to write out tons of type annotations all over the place.

Having never used dependent types, perhaps I'm just being romantic, but it seems that even having some constraints on just a few types (numerics, arrays/lists, perhaps strings), would be a great boon, and I hope one day we'll have a "commercial" (that is, useful with great tooling) language that supports dependent types.

I'd be happy with an extension to an existing language, that added a little new syntax. So you give the extended source to the new tool, it verifies type safety, and then strips the new syntax elements and passes it off to the original language's compiler. This can't be that hard, can it?

Microsoft Research created Spec#, which extends C# to have Eiffel-style contracts (pre- and post-conditions) specified above a function body. While the requires and ensures aren't dependent types, they do allow for extended static checking via Microsoft's Z3 theorem prover.

http://en.wikipedia.org/wiki/Spec_Sharp

Also check out F*

http://research.microsoft.com/en-us/projects/fstar/

This is part of Microsoft Research's big talk archive: http://research.microsoft.com/apps/dp/vi/videos.aspx

The archive has many great talks. For example if you're interested in compilers:

A recent great talk on a radically different way to do compiler optimization: http://research.microsoft.com/apps/video/default.aspx?id=162...

Another one on using Datalog for points-to analysis: http://research.microsoft.com/apps/video/default.aspx?id=103...

There are awesome talks on nearly any computer science topic (and also non-CS).

This was a great talk! I was excited to see that there's (or was) some work being done to extend GHC to support this: http://goto.ucsd.edu/~rjhala/liquid/

Sorry. Not as long as I have to install a special browser plugin to visit that page.

Ignore the plugin install then. Download links for text/slides/video are available in a number of formats in the bottom right hand corner of the page.

Are those video download links dead, or maybe just region-locked? Silverlight works fine, but they don't.

EDIT: Never mind, i can get them via my offshore VPS.

Oh, very nice. Is this related to the work on Liquid types for C at UCSD?

Thanks! It's great to see interest in our work on HN. Yes, this is the precursor to and basis for our current work on refinement type inference for C.

For those who haven't seen it, our recent work has focused on extending the automatic program verification techniques shown in this talk to work for low-level programs - that is, programs that use mutable state, pointer arithmetic, and so on. The project page for our Liquid Types-based verifier for C programs is here: http://goto.ucsd.edu/csolve/

The project page for the overall Liquid Types project is here: http://goto.ucsd.edu/~rjhala/liquid/

Silverlight. lol.

Reply on news.ycombinator.com