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

http://research.microsoft.com/apps/video/default.aspx?id=103638

by gtani • 14 years ago

79 14 14 years ago

research.microsoft.com

MrVitaliy• 14 years ago

Silverlight. lol.

MichaelGG• 14 years ago

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.

leif• 14 years ago

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?

chrisaycock• 14 years ago

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

gtani• 14 years ago

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

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

gambler• 14 years ago

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).

jberryman• 14 years ago

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/

jules• 14 years ago

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).

michaelfeathers• 14 years ago

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

voltagex_• 14 years ago

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.

eli_gottlieb• 14 years ago

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

pmrondon• 14 years ago

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/

mappu• 14 years ago

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.

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

Related Stories