Stars
LeanInteract: A Python Interface for Lean 4
Triton adapter for Ascend. Mirror of https://gitee.com/ascend/triton-ascend
Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
A statically-typed variant of Lox, written in TypeScript
RLinf is a flexible and scalable open-source infrastructure designed for post-training foundation models (LLMs, VLMs, VLAs) via reinforcement learning.
cuTile is a programming model for writing parallel kernels for NVIDIA GPUs
Agda lecture notes for the Functional Programming course at TU Delft
Envision a future where every student can read all the code of a teaching operating system.
CLI that compiles and runs CUDA C scripts on Modal GPUs
[NeurIPS 2025] PhysCtrl: Generative Physics for Controllable and Physics-Grounded Video Generation
Lean 4 kernel / 'external checker' written in Lean 4
Elixir is a dynamic, functional language for building scalable and maintainable applications
[ICRA, 2025] SplatSim: Zero-Shot Sim2Real Transfer of RGB Manipulation Policies Using Gaussian Splatting
TritonBench: Benchmarking Large Language Model Capabilities for Generating Triton Operators
A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.
A compiler, testing bed, and standard library for the Choral programming language.
ABC: System for Sequential Logic Synthesis and Formal Verification
(Mirror) A Machine-to-Machine Interaction System for Lean 4
AirPods liberated from Apple's ecosystem.