wasabi
@wasabi315.bsky.social
Published!!
dl.acm.org/doi/10.1145/...
dl.acm.org/doi/10.1145/...
October 10, 2025 at 2:32 AM
Published!!
dl.acm.org/doi/10.1145/...
dl.acm.org/doi/10.1145/...
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...
"Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search"
conf.researchr.org/details/icfp...
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...
conf.researchr.org
September 16, 2025 at 2:11 PM
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...
"Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search"
conf.researchr.org/details/icfp...
Now it reports all missing cases!
August 28, 2025 at 11:36 PM
Now it reports all missing cases!
Made compatible with agda2hs now so it compiles to readable Haskell!!
github.com/wasabi315/co...
github.com/wasabi315/co...
August 15, 2025 at 4:26 AM
Made compatible with agda2hs now so it compiles to readable Haskell!!
github.com/wasabi315/co...
github.com/wasabi315/co...
NbE for untyped lambda terms co-De Bruijn indices (in Haskell/Agda)!
Seems working!
github.com/wasabi315/ki...
github.com/wasabi315/ki...
Seems working!
github.com/wasabi315/ki...
github.com/wasabi315/ki...
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.
github.com
May 25, 2025 at 3:15 PM
NbE for untyped lambda terms co-De Bruijn indices (in Haskell/Agda)!
Seems working!
github.com/wasabi315/ki...
github.com/wasabi315/ki...
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...
github.com/wasabi315/ty...
March 25, 2025 at 3:22 AM
Added a search algorithm in which you can include variables to be unified in the query!
github.com/wasabi315/ty...
github.com/wasabi315/ty...
What would be the derivative of a higher inductive type?
February 27, 2025 at 12:53 PM
What would be the derivative of a higher inductive type?
Creating a collection of type-based library search algorithms🔍
It contains 3 algorithms with different search flexibility currently.
github.com/wasabi315/ty...
It contains 3 algorithms with different search flexibility currently.
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
github.com
February 18, 2025 at 12:19 AM
Creating a collection of type-based library search algorithms🔍
It contains 3 algorithms with different search flexibility currently.
github.com/wasabi315/ty...
It contains 3 algorithms with different search flexibility currently.
github.com/wasabi315/ty...
“Warnings for pattern matching”で提案されている網羅性アルゴリズムの一つをAgdaで形式化してる
停止性を除いて正当性を証明できた
github.com/wasabi315/ex...
停止性を除いて正当性を証明できた
github.com/wasabi315/ex...
GitHub - wasabi315/exhaustiveness-checking-agda
Contribute to wasabi315/exhaustiveness-checking-agda development by creating an account on GitHub.
github.com
December 12, 2024 at 9:16 AM
“Warnings for pattern matching”で提案されている網羅性アルゴリズムの一つをAgdaで形式化してる
停止性を除いて正当性を証明できた
github.com/wasabi315/ex...
停止性を除いて正当性を証明できた
github.com/wasabi315/ex...
TypeScriptの秘孔を突いてしまった
github.com/microsoft/Ty...
github.com/microsoft/Ty...
`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...
github.com
June 29, 2024 at 12:42 AM
TypeScriptの秘孔を突いてしまった
github.com/microsoft/Ty...
github.com/microsoft/Ty...
今から有限ステップで失敗するのと今失敗するのがpath equalなPartial Colist
github.com/wasabi315/ki...
github.com/wasabi315/ki...
kitchen-sink/agda/PartialTrunc.agda at main · wasabi315/kitchen-sink
Contribute to wasabi315/kitchen-sink development by creating an account on GitHub.
github.com
March 31, 2024 at 8:28 AM
今から有限ステップで失敗するのと今失敗するのがpath equalなPartial Colist
github.com/wasabi315/ki...
github.com/wasabi315/ki...
昔書いたSTGっぽい遅延評価機構 in JSの紹介を書いた
wasabi315.github.io/works/lazy/
wasabi315.github.io/works/lazy/
March 21, 2024 at 7:09 AM
昔書いたSTGっぽい遅延評価機構 in JSの紹介を書いた
wasabi315.github.io/works/lazy/
wasabi315.github.io/works/lazy/
RequiredTypeArguments拡張楽しみ〜
March 20, 2024 at 10:50 AM
RequiredTypeArguments拡張楽しみ〜
自分のウェブサイトAstroで書き直した
wasabi315.github.io
wasabi315.github.io
Home :: wasabi315
wasabi315's personal page
wasabi315.github.io
March 18, 2024 at 12:59 AM
自分のウェブサイトAstroで書き直した
wasabi315.github.io
wasabi315.github.io