2018-09-21 以降の追記事項

2018-09-21 追記

"5.5 A faster compiler" に関して, PDF版および arxiv 版では Error が生じます．そのため， Web page 記載の内容を見て訂正してください:

• 誤:

  1. compApp (Val n) c = comp (Val n) ++ c ==. ... ==. PUSH n:c
  2. compApp (Add x y) c = comp (Add x y) ++ c ==. ==. compApp x (compApp y (ADD:c))

• 正:

  1. compApp (Val n) c = comp (Val n) ++ c ==. ... ==. PUSH n:c `eq` PUSH n:c
  2. compApp (Add x y) c = comp (Add x y) ++ c ==. ==. compApp x (compApp y (ADD:c)) `eq` compApp x (compApp y (ADD:c))

2018-10-14 追記

skills matter にて，2018-10-14 ~ 2018-10-15 に行われたHaskell eXchange 2018における Keynote Liquid Haskell: Theorem Proving for All が公開されています（要: アカウント登録)．

勉強会の概要

『Haskellによる関数プログラミングの思考法』に関連する内容を学習します．

注意: 管理者のレベルの問題

• 管理者は，『Haskellによる関数プログラミングの思考法』の全ての等式論証を，スイスイ導出できません．
• Liquid Haskell を初めて使います

第34回の内容

『Haskellによる関数プログラミングの思考法』には，等式論証が数多くありました．

Liquid Haskell を用いたペーパーを読んでコードを書いて動作確認することにより，以下の項目を達成することが今回の目的です:

• 『Haskellによる関数プログラミングの思考法』の等式論証の復習
• Liquid Haskell の使い方の理解
• 『Haskellによる関数プログラミングの思考法』の一部を Liquid Haskell を用いて書き直す方法の理解

なお，今回が，この勉強会の最終回の予定です．

進め方

ペーパー (PDF) に記載されている必要そうな記述内容を，主催者が音読して読み進める予定です．

扱う内容

"Theorem Proving for All - Equational Reasoning in Liquid Haskell"(Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, and Graham Hutton; 2018)

但し，"6.Related Work" の章は扱いません．

• Web page
• PDF
• arxiv.org

注意

• 間違った説明を行なってしまった際に，その指摘をすることを歓迎します。

タイムスケジュール

その他

• 参加者の半数に通信障害が生じ 10分間その状況が継続しているなど， 勉強会を継続することが困難または好ましくないと判断できる事由が生じた場合，その日の勉強会を終了 することがあります。

• 質問の回答を，別の参加者の方にお願いすることがあります。