Niki Vazou's guest appearances

Niki Vazou

Functional Geekery

CoRecursive: Coding Stories

Bruce Tate

Philip Wadler

Zach Tellman

Jared Forsyth

Gabriel Gonzalez

Justin Woo

Bartosz Milewski

Andy Hunt

Edwin Brady

Chris Allen

Colin Barrett

ERIC SMITH

Gene Kim

Evan Hubinger

Colin Jones

OwlTail

Formal verification and type systems - how do they relate? Niki Vazou is on a mission to bring better formal verification to the masses. I have done a couple of episodes about dependent types and my feeling is that dependent types are super powerful and have some conceptual simplicity ( Types are a first-class concept ) but are somewhat tricky to wield in practice. Refinement types are something simpler. A refinement is a predicate that narrows the meaning of a type. What if instead of divide taking two ints, one was Int i where i != 0. This is a refinement type, a type that has been refined, the set of possible values narrowed, using simple predicates. Niki is the creator of Liquid Haskell, a system that extends Haskell to support refinements. It actually goes farther than that. She has also worked on refinement types in Ruby and explained refinement types to scala community at various conferences, but her heart lies with the Haskell community. We talk about refinement types, theorem proving, formal verification, SMT solvers, and working with GHC. This interview is also a great place to hear me asking stupid questions of a very smart person. Niki and her work are way outside my comfort bounds but hopefully my struggles to understand the topic will help make the power of refinement types approachable to a wider audience. Ruby developers, js developers, and everyone, refinement types are for you as well. Links:  Liquid Haskell Talk Programming with Refinement Types Liquid Haskell Tutorial Niki's Ph.D. Thesis Real World Liquid Types Refinement Types for Ruby Liquid Haskell Proofs Refinement Types for Scala  

Formal verification and type systems - how do they relate? Niki Vazou is on a mission to bring better formal verification to the masses. I have done a couple of episodes about dependent types and my feeling is that dependent types are super powerful and have some conceptual simplicity ( Types are a first-class concept ) but are somewhat tricky to wield in practice. Refinement types are something simpler. A refinement is a predicate that narrows the meaning of a type. What if instead of divide taking two ints, one was Int i where i != 0. This is a refinement type, a type that has been refined, the set of possible values narrowed, using simple predicates. Niki is the creator of Liquid Haskell, a system that extends Haskell to support refinements. It actually goes farther than that. She has also worked on refinement types in Ruby and explained refinement types to scala community at various conferences, but her heart lies with the Haskell community. We talk about refinement types, theorem proving, formal verification, SMT solvers, and working with GHC. This interview is also a great place to hear me asking stupid questions of a very smart person. Niki and her work are way outside my comfort bounds but hopefully my struggles to understand the topic will help make the power of refinement types approachable to a wider audience. Ruby developers, js developers, and everyone, refinement types are for you as well. Links: <ul> <li><a href="https://www.youtube.com/watch?v=SmRo7q_6oG8&amp;t=285s" rel="nofollow" target="_blank">Liquid Haskell Talk</a></li> <li><a href="http://ucsd-progsys.github.io/lh-workshop/" rel="nofollow" target="_blank">Programming with Refinement Types</a></li> <li><a href="http://ucsd-progsys.github.io/liquidhaskell-tutorial/" rel="nofollow" target="_blank">Liquid Haskell Tutorial</a></li> <li><a href="http://goto.ucsd.edu/~nvazou/thesis/main.pdf" rel="nofollow" target="_blank">Niki's Ph.D. Thesis</a></li> <li><a href="http://goto.ucsd.edu/~nvazou/real_world_liquid.pdf" rel="nofollow" target="_blank">Real World Liquid Types</a></li> <li><a href="https://nikivazou.github.io/static/VMCAI18/paper.pdf" rel="noopener nofollow" target="_blank">Refinement Types for Ruby</a></li> <li><a href="https://www.youtube.com/watch?v=fRBIR2RJIIo" rel="nofollow" target="_blank">Liquid Haskell Proofs</a></li> <li><a href="https://github.com/fthomas/refined" rel="nofollow" target="_blank">Refinement Types for Scala </a></li> </ul>

Refinement Types and Liquid Haskell With Niki Vazou

In this episode I talk with Niki Vazou.  We talk about her introduction to Haskell, Ph.D. and graduate school overview, and all things Liquid Haskell. Our Guest, Niki Vazou @nikivazou on Twitter https://nikivazou.github.io/ Liquid Haskell website Announcements Kats Conf 2 will be taking place in Dublin, Ireland on the 18th of February.  Visit http://www.katsconf.com/ to register and for more information. ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany.  Visit www.clojured.de to get tickets and keep updated as more information becomes available. BOB Konf is taking place the 24th of February 2017 in Berlin, Germany.  Visit www.bobkonf.de for more information about the conference. ElixirDaze is coming up on March 2nd and 3rd.  With keynotes by Prag Dave Thomas and Saša Jurić, make sure to visit www.elixirdaze.com for more information and to register. Destination Code, a new unconference starting in Utah, is having its inaugural event March 27-30th, 2017. Visit http://www.destination.codes/ to find out more. Erlang &amp; Elixir Factory 2017 is on the 23rd and 24th of March. Visit www.erlang-factory.com/sfbay2017 for more information. The O’Reilly Software Architecture Conference will be taking place April 2-5, 2017 in New York. Visit http://www.oreilly.com/pub/cpc/50017 to register and find out more, and use code USRG for 20% off most passes. flatMap(Oslo) is a FP-conference with focus on Scala and the JVM, taking place on May 2nd and 3rd in Oslo, Norway. Please go to http://2017.flatmap.no/cfp/ to learn more. ElixirConf EU will be taking place on May 4th and 5th with tutorials on May 3rd.  For more information visit: http://www.elixirconf.eu/ OSCON will be taking place May 8-11 in Austin, TX. For more information and to register visit: http://www.oreilly.com/pub/cpc/50016, and use code USRG for 20% off most passes. Elm Europe will be taking place June 8th and 9th in Paris, France.  Visit http://elmeurope.org/ for more information and to register.   EuroClojure will be taking place in Berlin, Germany on July 20th &amp; 21st. Visit http://2017.euroclojure.org/ for more information and to keep updated. If you have a conference related to functional programming, contact me, and I will be happy to announce it. Topics [@5:49] About Niki Liquid Haskell Simon Peyton Jones on Episode 11 mentioning Liquid Haskell Niki’s Thesis Niki’s introduction to Haskell Liquid Types paper Liquid Types for OCaml What made Haskell click for Niki Coming in and understanding Types in Haskell Hoogle Monads and `do` notation How Niki was introduced to working on Liquid Types in Haskell Overview of how graduate school projects generally work Overview of Liquid Haskell Refinement types Heartbleed SMT Solver “Liquid Haskell is basically Haskell […] extended with special comments in which the user can give their Refinement Type specifications” Difference between Dependent Types, Refinement Types, and Liquid Types Decidable Theory Specifying specifications to help make sure the SMT solver has enough information to determine code is `safe` Gabriel Gonzalez – Compile-time memory safety using Liquid Haskell Gradual Typing Running Liquid Haskell at the module level Liquid Haskell `assume` keyword Interacting with code that has yet to be annotated with Liquid Haskell Working on specifications for recursive functions “You can treat Liquid Haskell as a theorem prover” Ability to start using Liquid Haskell from the beginning The feedback cycle between the research and industry in the Haskell community Where to find out more about Liquid Haskell Liquid Haskell website Liquid Haskell blog Liquid Haskell About page Try Liquid Haskell online Liquid Haskell tutorial Liquid Haskell Github repo Liquid Haskell mailing list Niki at Lambda Days Niki keynoting at Typelevel Summit Niki at Programming Language Design and Implementation 2017 As always, a giant Thank You goes to David Belcher for the logo design.

In this episode I talk with Niki Vazou. We talk about her introduction to Haskell, Ph.D. and graduate school overview, and all things Liquid Haskell. <h2>Our Guest, Niki Vazou</h2> <a href="https://twitter.com/nikivazou" rel="noopener noreferrer nofollow" target="_blank">@nikivazou</a> on Twitter <a href="https://nikivazou.github.io/" rel="noopener noreferrer nofollow" target="_blank">https://nikivazou.github.io/</a> <a href="https://ucsd-progsys.github.io/liquidhaskell-blog/" rel="noopener noreferrer nofollow" target="_blank">Liquid Haskell website</a> <h3>Announcements</h3> Kats Conf 2 will be taking place in Dublin, Ireland on the 18th of February. Visit <a href="http://www.katsconf.com/" rel="noopener noreferrer nofollow" target="_blank">http://www.katsconf.com/</a> to register and for more information. ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany. Visit <a href="http://www.clojure.de" rel="noopener noreferrer nofollow" target="_blank">www.clojured.de</a> to get tickets and keep updated as more information becomes available. BOB Konf is taking place the 24th of February 2017 in Berlin, Germany. Visit <a href="http://www.bobkonf.de" rel="noopener noreferrer nofollow" target="_blank">www.bobkonf.de</a> for more information about the conference. ElixirDaze is coming up on March 2nd and 3rd. With keynotes by Prag Dave Thomas and Saša Jurić, make sure to visit <a href="http://www.elixirdaze.com" rel="noopener noreferrer nofollow" target="_blank">www.elixirdaze.com</a> for more information and to register. Destination Code, a new unconference starting in Utah, is having its inaugural event March 27-30th, 2017. Visit <a href="http://www.destination.codes/" rel="noopener noreferrer nofollow" target="_blank">http://www.destination.codes/</a> to find out more. Erlang &amp; Elixir Factory 2017 is on the 23rd and 24th of March. Visit <a href="http://www.erlang-factory.com/sfbay2017" rel="noopener noreferrer nofollow" target="_blank">www.erlang-factory.com/sfbay2017</a> for more information. The O’Reilly Software Architecture Conference will be taking place April 2-5, 2017 in New York. Visit <a href="http://www.oreilly.com/pub/cpc/50017" rel="noopener noreferrer nofollow" target="_blank">http://www.oreilly.com/pub/cpc/50017</a> to register and find out more, and use code USRG for 20% off most passes. flatMap(Oslo) is a FP-conference with focus on Scala and the JVM, taking place on May 2nd and 3rd in Oslo, Norway. Please go to <a href="http://2017.flatmap.no/cfp/" rel="noopener noreferrer nofollow" target="_blank">http://2017.flatmap.no/cfp/</a> to learn more. ElixirConf EU will be taking place on May 4th and 5th with tutorials on May 3rd. For more information visit: <a href="http://www.elixirconf.eu/" rel="nofollow" target="_blank">http://www.elixirconf.eu/</a> OSCON will be taking place May 8-11 in Austin, TX. For more information and to register visit: <a href="http://www.oreilly.com/pub/cpc/50016" rel="noopener noreferrer nofollow" target="_blank">http://www.oreilly.com/pub/cpc/50016</a>, and use code USRG for 20% off most passes. Elm Europe will be taking place June 8th and 9th in Paris, France. Visit <a href="http://elmeurope.org/" rel="noopener noreferrer nofollow" target="_blank">http://elmeurope.org/</a> for more information and to register. EuroClojure will be taking place in Berlin, Germany on July 20th &amp; 21st. Visit <a href="http://2017.euroclojure.org/" rel="noopener noreferrer nofollow" target="_blank">http://2017.euroclojure.org/</a> for more information and to keep updated. If you have a conference related to functional programming, contact me, and I will be happy to announce it. <h3>Topics [@5:49]</h3> About Niki <a href="https://ucsd-progsys.github.io/liquidhaskell-blog/" rel="noopener noreferrer nofollow" target="_blank">Liquid Haskell</a> <a href="https://www.functionalgeekery.com/episode-11-simon-peyton-jones/" rel="noopener noreferrer nofollow" target="_blank">Simon Peyton Jones on Episode 11</a> mentioning Liquid Haskell <a href="http://goto.ucsd.edu/~nvazou/thesis/main.pdf" rel="noopener noreferrer nofollow" target="_blank">Niki’s Thesis</a> Niki’s introduction to Haskell <a href="http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf" rel="noopener noreferrer nofollow" target="_blank">Liquid Types paper</a> Liquid Types for OCaml What made Haskell click for Niki Coming in and understanding Types in Haskell <a href="https://www.haskell.org/hoogle/" rel="noopener noreferrer nofollow" target="_blank">Hoogle</a> Monads and `do` notation How Niki was introduced to working on Liquid Types in Haskell Overview of how graduate school projects generally work Overview of Liquid Haskell Refinement types <a href="http://heartbleed.com/" rel="noopener noreferrer nofollow" target="_blank">Heartbleed</a> SMT Solver “Liquid Haskell is basically Haskell […] extended with special comments in which the user can give their Refinement Type specifications” Difference between Dependent Types, Refinement Types, and Liquid Types Decidable Theory Specifying specifications to help make sure the SMT solver has enough information to determine code is `safe` <a href="http://www.haskellforall.com/2015/12/compile-time-memory-safety-using-liquid.html" rel="noopener noreferrer nofollow" target="_blank">Gabriel Gonzalez – Compile-time memory safety using Liquid Haskell</a> Gradual Typing Running Liquid Haskell at the module level Liquid Haskell `assume` keyword Interacting with code that has yet to be annotated with Liquid Haskell Working on specifications for recursive functions “You can treat Liquid Haskell as a theorem prover” Ability to start using Liquid Haskell from the beginning The feedback cycle between the research and industry in the Haskell community Where to find out more about Liquid Haskell <a href="https://ucsd-progsys.github.io/liquidhaskell-blog/" rel="noopener noreferrer nofollow" target="_blank">Liquid Haskell website</a> <a href="https://ucsd-progsys.github.io/liquidhaskell-blog/blog.html" rel="noopener noreferrer nofollow" target="_blank">Liquid Haskell blog</a> <a href="https://ucsd-progsys.github.io/liquidhaskell-blog/about.html" rel="noopener noreferrer nofollow" target="_blank">Liquid Haskell About page</a> <a href="http://goto.ucsd.edu:8090/index.html#?demo=SimpleRefinements.hs" rel="noopener noreferrer nofollow" target="_blank">Try Liquid Haskell online</a> <a href="https://ucsd-progsys.github.io/lh-workshop/" rel="noopener noreferrer nofollow" target="_blank">Liquid Haskell tutorial</a> <a href="https://github.com/ucsd-progsys/liquidhaskell" rel="noopener noreferrer nofollow" target="_blank">Liquid Haskell Github repo</a> <a href="https://groups.google.com/forum/#!forum/liquidhaskell" rel="noopener noreferrer nofollow" target="_blank">Liquid Haskell mailing list</a> <a href="http://www.lambdadays.org/lambdadays2017/niki-vazou" rel="noopener noreferrer nofollow" target="_blank">Niki at Lambda Days</a> <a href="http://typelevel.org/event/2017-03-summit-nyc/" rel="noopener noreferrer nofollow" target="_blank">Niki keynoting at Typelevel Summit</a> <a href="http://pldi17.sigplan.org/profile/nikivazou" rel="noopener noreferrer nofollow" target="_blank">Niki at Programming Language Design and Implementation 2017</a> As always, a giant Thank You goes to <a href="https://www.twitter.com/davidjbelcher" rel="noopener noreferrer nofollow" target="_blank">David Belcher</a> for the logo design.

Functional Geekery Episode 84 - Niki Vazou