タグ: #liquid-haskell

← すべての記事

• モダンHaskell 2026 — GHC 9.10 / 9.12 / GHCup / Cabal 3.14 / Stack / IHP / Servant / Effectful / Pandoc / Cardano 徹底ガイド

  2026年のHaskellは「博士号を持つ人が論文を書くために使う言語」ではない。GHC 9.10(2024年5月)と9.12(2024年12月)でコンパイラはもう一段速くなり、GHCupが公式推奨インストーラとして定着したことで、Cabal 3.14とStackの選択は単純になった。IHPがRails級のフルスタック体験を提供し、Servantが型付きHTTP APIの標準となり、Effectfulがmtlスタイルを急速に置き換えてい

  2026-05-16 · 27 分で読めます #haskell#ghc-9-10#ghc-9-12#ghcup#cabal

• Lean 4 & 定理証明支援系 2026 — mathlib / Rocq (旧 Coq) / Agda / Isabelle / FStar / AlphaProof / AIMO 深掘りガイド

  2026年、定理証明支援系(proof assistant)はもはや学界の秘密兵器ではない。Lean 4 は Leonardo de Moura が AWS に移って以来爆発的に成長し、mathlib は 100 万定理を超え、Terence Tao を含む一流数学者の日常の道具となった。Coq は 2024 年 3 月に Rocq へリブランドを完了し、Agda・Idris 2・Isabelle/HOL はそれぞれの位置を保つ。Mic

  2026-05-16 · 35 分で読めます #lean-4#lean#mathlib#rocq#coq