{"id":4731,"date":"2015-01-19T10:22:42","date_gmt":"2015-01-19T09:22:42","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4731"},"modified":"2015-01-19T10:22:42","modified_gmt":"2015-01-19T09:22:42","slug":"resena-liquidhaskell-refinement-types-in-the-real-world","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-liquidhaskell-refinement-types-in-the-real-world\/","title":{"rendered":"Rese\u00f1a: LiquidHaskell: Refinement types in the real world"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo sobre verificaci\u00f3n de programas Haskell con <a href=\"http:\/\/goto.ucsd.edu\/~rjhala\/liquid\/haskell\/blog\/about\">LiquidHaskell<\/a> titulado <a href=\"http:\/\/bit.ly\/1GeNHaP\">LiquidHaskell: Refinement types in the real world<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/goto.ucsd.edu\/~nvazou\">Niki Vazou<\/a>, <a href=\"http:\/\/eric.seidel.io\">Eric L. Seidel<\/a> y <a href=\"http:\/\/goto.ucsd.edu\/~rjhala\">Ranjit Jhala<\/a> (de la Univ. de California en San Diego).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  Haskell has many delightful features. Perhaps the one most beloved by its users is its type system that allows developers to specify and verify a variety of program properties at compile time. However, many properties, typically those that depend on relationships between program values are impossible, or at the very least, cumbersome to encode within the existing type system. Many such properties can be verified using a combination of Refinement Types and external SMT solvers. We describe the refinement type checker <a href=\"http:\/\/goto.ucsd.edu\/~rjhala\/liquid\/haskell\/blog\/about\">LiquidHaskell<\/a>, that we have used to specify and verify a variety of properties of over 10,000 lines of Haskell code from various popular libraries, including containers, hscolour, bytestring, text, vector-algorithms and xmonad. First, we present a high-level overview of LiquidHaskell , through a tour of its features. Second, we present a qualitative discussion of the kinds of properties that can be checked \u2013 ranging from generic application independent criteria like totality and termination, to application specific concerns like memory safety and data structure correctness invariants. Finally, we present a quantitative evaluation of the approach, with a view towards measuring the efficiency and programmer\u2019s effort required for verification, and discuss the limitations of the approach.\n<\/p><\/blockquote>\n<p>El trabajo se ha presentado en el <a href=\"http:\/\/bit.ly\/1BTarJm\">ACM Haskell Symposium 2014<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo sobre verificaci\u00f3n de programas Haskell con LiquidHaskell titulado LiquidHaskell: Refinement types in the real world. Sus autores son Niki Vazou, Eric L. Seidel y Ranjit Jhala (de la Univ. de California en San Diego). Su resumen es Haskell has many delightful features. Perhaps the one most beloved by its users&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[270,242,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4731"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4731"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4731\/revisions"}],"predecessor-version":[{"id":4732,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4731\/revisions\/4732"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4731"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4731"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4731"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}