4 ms·

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

79 points by gtani 15y ago

MrVitaliy 15y ago
Silverlight. lol.
MichaelGG 15y 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 15y 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 15y 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 http://en.wikipedia.org/wiki/Spec_Sharp
    - Rickasaurus 15y ago
      Also check out F* http://research.microsoft.com/en-us/projects/fstar/ http://research.microsoft.com/en-us/projects/fstar/
gtani 15y ago
http://goto.ucsd.edu/~pmr/papers/liquid-types-pldi08.pdf http://goto.ucsd.edu/~pmr/papers/liquid-types-pldi08.pdf Probably should have noted submitted URL is Silverlight video, or large download.
gambler 15y 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 15y 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/ http://goto.ucsd.edu/~rjhala/liquid/
jules 15y ago
This is part of Microsoft Research's big talk archive: http://research.microsoft.com/apps/dp/vi/videos.aspx 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=162853&l=i 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=103389&l=i 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 15y ago
Sorry. Not as long as I have to install a special browser plugin to visit that page.
- voltagex_ 15y 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 15y ago
Oh, very nice. Is this related to the work on Liquid types for C at UCSD?
- pmrondon 15y 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/ http://goto.ucsd.edu/csolve/ The project page for the overall Liquid Types project is here: http://goto.ucsd.edu/~rjhala/liquid/ http://goto.ucsd.edu/~rjhala/liquid/
mappu 15y 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.

79 points by gtani 15y ago

Silverlight. lol.

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 15y 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 15y 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 http://en.wikipedia.org/wiki/Spec_Sharp
  - Rickasaurus 15y ago
    Also check out F* http://research.microsoft.com/en-us/projects/fstar/ http://research.microsoft.com/en-us/projects/fstar/

gtani 15y ago

http://goto.ucsd.edu/~pmr/papers/liquid-types-pldi08.pdf http://goto.ucsd.edu/~pmr/papers/liquid-types-pldi08.pdf Probably should have noted submitted URL is Silverlight video, or large download.

gambler 15y 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 15y 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/ http://goto.ucsd.edu/~rjhala/liquid/

jules 15y ago

This is part of Microsoft Research's big talk archive: http://research.microsoft.com/apps/dp/vi/videos.aspx 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=162853&l=i 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=103389&l=i 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 15y ago

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

voltagex_ 15y 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 15y ago

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

pmrondon 15y 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/ http://goto.ucsd.edu/csolve/ The project page for the overall Liquid Types project is here: http://goto.ucsd.edu/~rjhala/liquid/ http://goto.ucsd.edu/~rjhala/liquid/

mappu 15y 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.