Stars
Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.
Fork of Plan 9 meant for education. https://principia-softwarica.org/
A spreadsheet implementation in Rocq, extracted to C++ via Crane.
A fast terminal spreadsheet editor with Vim keybindings
A parser based on the ALL(*) algorithm, implemented and verified in Coq.
Initial release: constructive proof of Rice's theorem via MRDP
A minimal Scheme to embed Rocq extracted code into constrained targets
A parser, formatter, validator, and language server for SQLite SQL. Built on SQLite's own grammar and tokenizer
The 1SubML programming language - unified module and value language, structural subtyping, global type inference, higher rank polymorphic types, existential types, higher kinded types (no partial a…
Outcome logic formalization in Rocq (OOPSLA '23)
Tools for MIL, a Monadic Intermediate Language
an embedded os written in haskell with microhs with lisp support, cs140e final project
🌸 Learn Japanese grammar with TypeScript
Lean playground for programming language modeling tooling.
Emdash is the Open-Source Agentic Development Environment (🧡 YC W26). Run multiple coding agents in parallel. Use any provider.
Local codebase intelligence CLI + MCP server for AI coding agents: SQLite code graph, 28 languages, 238 commands, 224 MCP tools, change-safety gates, audit evidence, zero API keys.
Manage multiple AI terminal agents like Claude Code, Codex, OpenCode, and Amp.
mirror of Fabrice Bellard's libbf tar releases, with fixes and CI
Haskell package for construction and running of finite state transducers.
Verified extraction of neural network weights from Coq proofs to deployable formats
IsoCity: City building simulation game.
An ascii (ratatui) physics based render engine for graphs (petgraph)
A type-safe, component-based language for building reactive WASM web apps.