wasabi

Happy new year🎉

A Verified Coverage Checker Formalizing a pattern-matching coverage-checking algorithm in Agda

Wrote a post on a verified pattern-matching coverage checker!
wasabi315.github.io/en/posts/ver...

(英語版も見れるようにしました！ChatGPT様様...)

検証付きカバレッジ検査器 パターンマッチのCoverage CheckingアルゴリズムをAgdaで形式化した

パターンマッチのカバレッジ検査の verified implementationをAgdaでした話をブログに書きました！
wasabi315.github.io/ja/posts/ver...

Published!!
dl.acm.org/doi/10.1145/...

Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search (TyDe 2025) - ICFP/SPLASH 2025 The Workshop on Type-Driven Development (TyDe) aims to show how static type information may be used effectively in the development of computer programs. Co-located with ICFP, this workshop brings toge...

Excited to present at TyDe2025 in Singapore this October!
"Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search"

conf.researchr.org/details/icfp...

Now it reports all missing cases!

Made compatible with agda2hs now so it compiles to readable Haskell!!
github.com/wasabi315/co...

停止性も証明できた！

kitchen-sink/haskell/co-debruijn/app/Main.hs at main · wasabi315/kitchen-sink Contribute to wasabi315/kitchen-sink development by creating an account on GitHub.

NbE for untyped lambda terms co-De Bruijn indices (in Haskell/Agda)!
Seems working!
github.com/wasabi315/ki...
github.com/wasabi315/ki...

Added a search algorithm in which you can include variables to be unified in the query!
github.com/wasabi315/ty...

Added an algorithm for dependent types!
github.com/wasabi315/ty...

What would be the derivative of a higher inductive type?

Added an algorithm for SystemF!
github.com/wasabi315/ty...

GitHub - wasabi315/type-search-zoo: A collection of type-based library search algorithms A collection of type-based library search algorithms - wasabi315/type-search-zoo

Creating a collection of type-based library search algorithms🔍
It contains 3 algorithms with different search flexibility currently.
github.com/wasabi315/ty...

網羅性検査を実際に動かしてる例

“Warnings for pattern matching”で提案されている網羅性アルゴリズムの一つをAgdaで形式化してる
停止性を除いて正当性を証明できた
github.com/wasabi315/ex...

GitHub - wasabi315/dependent-type-check-ts Contribute to wasabi315/dependent-type-check-ts development by creating an account on GitHub.

TypeScriptで依存型の型検査器を書いてる
今のところは自然数とequalityが入っている
github.com/wasabi315/de...

`getTypeListId` crashes with `TypeError: Cannot read properties of undefined (reading 'id')` · Issue #59062 · microsoft/TypeScript 🔎 Search Terms getTypeListId, circular reference, conditional types 🕗 Version & Regression Information This is a crash This changed between versions (confirmed using the Playground) ~3.6.3: does no...

TypeScriptの秘孔を突いてしまった
github.com/microsoft/Ty...

GitHub - wasabi315/lazy: STG-like lazy evaluation mechanism in JavaScript STG-like lazy evaluation mechanism in JavaScript. Contribute to wasabi315/lazy development by creating an account on GitHub.

リポジトリ: github.com/wasabi315/lazy

そういえば分割束縛できる機能もつけた、ちゃんとlazyなパターンマッチになってる
画像はTardisモナドのbindの実装

kitchen-sink/agda/PartialTrunc.agda at main · wasabi315/kitchen-sink Contribute to wasabi315/kitchen-sink development by creating an account on GitHub.

今から有限ステップで失敗するのと今失敗するのがpath equalなPartial Colist
github.com/wasabi315/ki...

GitHub - clayrat/guarded-cm: Experiments with guarded recursion Experiments with guarded recursion. Contribute to clayrat/guarded-cm development by creating an account on GitHub.

👀 github.com/clayrat/guar...

昔書いたSTGっぽい遅延評価機構 in JSの紹介を書いた
wasabi315.github.io/works/lazy/

RequiredTypeArguments拡張楽しみ〜

ErlangのVMで動くからDistributedなSignalがあると面白いかも…？(Signal同士がmessage passingで更新情報を送り合う感じ)

全然記事書いてないので今後書く

自分のウェブサイトAstroで書き直した
wasabi315.github.io