Hiromi Ishii

computational-algebra. General-Purpose Computer Algebra System as an EDSL in Haskell

equational-reasoning-in-haskell. Agda-style equational reasoning in Haskell

type-natural. Type-level well-kinded natural numbers.

qualified_do. Rust

ad-delcont-primop. Haskell

smooth. Exploring connections between automatic differentiation and smooth infinitesimal analysis, or smooth algebras

ghc-wasm-earthly. GHC WASM backend made easy to use for platforms without precompiled bindists powered by Earthly

satysfi-steamer. Steamer: presentation in SATySFi

linear-extra. Missing utilities for Linear Haskell, for array, witness token, memory, parallelism, and streaming.

Yablog. Yet another Blog engine written in Haskell powered by yesod.

humblr. Haskell

sdg-agda. Synthetic Differential Geometry in Agda

sized. Sized sequence data-types

herbrand. An experiment around automated theorem proving in Haskell

vscode-generic-input-method. Generic Input Method for VSCode, mainly focusing on Unicode Symbol input for Theorem Provers, and YaTeX-like image completion for LaTeX

pandoc-japanese-filters. Pandoc filters to treat Japanese-specific markups

ghc-typelits-presburger. Presburger arithmetic solver for built-in type-level naturals

category-agda. Category Theory in Agda

dl-first-principle-tutorial. A record of my struggling of learning Deep Learning, following the tutorial series "10 Days Of Grad: Deep Learning From The First Principles" by Bogdan Penkovsky.

lambda-pi. My hobby implementation of dependent-type system

skolem-rs. DPLL and CDCL SAT solver written in Rust

subcategories. Functors on subcategories induced by class constraints

servant-cloudflare-workers. Haskell

hagi. HaGi - Haskell Grass Interpreter

sized-vector. DEPRECATED: use `sized` package instead

hskk. SKK implemented in Haskell

newtype-talk-five. Haskell's newtype functionality and DerivingVia explained (Japanese talk at FIVE)

sake. Sake is a static-site generator built on top of the Shake build system.

FRP2048. Demo of GHCJS, Sodium and extensible-effects (a clone of 2048)

AttoJSON. ByteString based lightweight JSON Parser

fluent-plugin-amqp. TODO: one-line summary of your gem

safe-printf. Well-typed, flexible and variadic printf in Haskell.

laurent. Formal power series and Laurent series, cubically

lk-proof-assistant. Simple Proof assistant for LK Calculus (First-Order logic)

ghc-typelits-symbols. Additional operations for GHC's type-level symbols

hastr. Haskell Nostr Implementation

multisock. Reverse Proxy / Multiplexer for UNIX Domain Socket, mainly targeted to gpg-agent

TAOP-Exercises. The Answer code for "The Art Of Prolog(2nd Ed)" Exercises.

HoTwitter. Simple Twitter client Written In HOC (Haskell Objective-C binding)

party-ferris. An emoji of Ferris dancing so happily

rupircd. RUby Pseudo IRC Daemon

BottleStory. A Simple Relay Novel Writing System

grasuby. grasuby - GRASs rUBY interpreter and his firends

hsosa. Haskell Interface for OS X Open Scripting Architecture (OSA, AppleScript)

Quasi-Quote-Examples. Examples for my article

gitolist. A web frontend for gitolite

haskell-smtp. SMTP libraries for SMTP.

pandoc-japanese-docx. Enhanced Docx reader for pandoc with the support for Japanese markups

foldl-extras. A utility package to work comfortably with foldl package