Back in May, I gave the opening keynote (my first keynote talk!) at the FLOPS 2022 conference. I talked about the work we’ve been doing in my group on using Liquid Haskell for verifying the correctness of distributed systems. Here’s a pseudo-transcript1 of my FLOPS talk. Some of the slides are included below, and I’ve posted the full set of slides as well. Good morning Good morning, FLOPS! Good mo
Since the inception of the Haskell language, the community around it has steadily innovated with language extensions and abstractions. To mention a few, we had the IO monad, all flavors of type classes and constraints, Template Haskell, generalized algebraic data types (GADTs), data kinds, etc. Then we had to deal with the programs resulting from all this innovation, which eventually sprang feelin
LiquidHaskell is a GHC Plugin Posted by Ranjit Jhala Aug 20, 2020 I enjoy working with LH. However, I’d be the very first to confess that it has been incredibly tedious to get to work on existing code bases, for various reasons. LH ran one file at a time; it was a hassle to systematically analyze all the modules in a single package. LH had no notion of packages; it was impossible to import specifi
Theorem Proving for All Equational Reasoning in Liquid Haskell Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, and Graham Hutton [PDF] 1.Introduction 2.Reasoning about Programs 2.1. Lightweight Reasoning 2.2. Induction on Lists 2.3. Proof Automation 3.Totality and Termination 3.1. Totality Checking 3.2. Termination Checking 3.3. Uncaught termination 4.Function Optimization 4.1. Example:
Liquid Haskell Tutorial BOB 2018, Berlin, 2018-02-23 Andres Löh Acknowledgements Thanks to the entire Liquid Haskell team for producing such a fantastic tool, including the interactive web environment used for this tutorial. Special thanks to Ranjit Jhala and Niki Vazou for tirelessly answering all my questions during the preparation of this tutorial. Contents 1. Introduction 1.1. What is Liquid H
A Tale of Two Provers Verifying Monoidal String Matching in Liquid Haskell and Coq Niki Vazou University of Maryland Leonidas Lampropoulos University of Pennsylvania Jeff Polakow Awake Networks Abstract We demonstrate for the first time that Liquid Haskell, a refinement type checker for Haskell programs, can be used for arbitrary the- orem proving by verifying a parallel, monoidal string matching
このエントリは Haskell Advent Calendar 2016 および Formal Method Advent Calendar 2016 の 23 日目の投稿です。のはずでしたがすでに日付が変わりました。謹んでお詫び申し上げます。 ちなみに 22 日目の担当者はそれぞれ Haskell Advent Calendar 2016 : heredocsの紹介 - Qiita Formal Method Advent Calendar 2016 : 農夫 山羊 キャベツ 狼 - Qiita です。偶然ですが同じ方が執筆担当ですね。 さて、本エントリでは Haskell の型の表現力をより豊かにする仕組み、 LiquidHaskell について概要を紹介します。使用するサンプルコードは Samples of Verification by LiquidHaskell · GitHub
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
