A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.

Lean lens implementation with custom notation.

Verified GPU programming framework for Lean 4. Write type-safe WebGPU shaders with formal verification, hardware-accelerated matrix ops, and cross-platform support (Metal/Vulkan/D3D12). Build prova…

A list of paper templates in the area of machine learning.

Lobster: A GPU-Accelerated Framework for Neurosymbolic Programming

formalization of music theory

(Mirror) A Music formalization library and DSL in Lean 4

Tensors and neural networks in Haskell

Tracking publicly disclosed bugs found with Xint

A Testing Framework for Lean

The Lean Computer Science Library (CSLib)

Chess in Lean 4

Agent skills for Obsidian. Teach your agent to use Markdown, Bases, JSON Canvas, and use the CLI.

Running TCP/IP over SWD lines

SystemVerilog to Verilog conversion

Functional Reactive Programming domain-specific language for efficient hybrid systems

Software synthesizer

PPL サマースクール 2025 の資料置き場です。

The sound of soundness. An interactive music player for Rocq Proofs.

Formalization of Mathematical Logic

The Ott tool for writing definitions of programming languages and calculi

The fifth iteration of Pitaya

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

Natural language tactics to teach mathematics using Lean 4

CIS 7000-01 Fall 2025 Course materials

Template for Lean<->Rust FFI

Utilities and reasoning principles for monads in Coq

Sound As Pure Form - a Forth-like language for audio synthesis using lazy lists and APL-like auto-mapping.

A client for Language Server Protocol servers