Highlights
- Pro
Stars
- All languages
- ATS
- Agda
- Assembly
- C
- C#
- C++
- CSS
- Clojure
- CoffeeScript
- Common Lisp
- Coq
- Crystal
- Dafny
- Dockerfile
- Elm
- Emacs Lisp
- Erlang
- F*
- Frege
- Go
- Grammatical Framework
- HTML
- Haskell
- Idris
- Janet
- Java
- JavaScript
- Jupyter Notebook
- Koka
- Kotlin
- LLVM
- Lean
- LiveScript
- Lua
- MATLAB
- MDX
- Makefile
- Mathematica
- Nearley
- Nix
- Nunjucks
- OCaml
- Objective-C
- Opa
- OpenSCAD
- Perl
- PostScript
- Prolog
- PureScript
- Python
- Racket
- Reason
- Rocq Prover
- Ruby
- Rust
- SMT
- Scala
- Scheme
- Shell
- Standard ML
- Swift
- SystemVerilog
- TeX
- TypeScript
- UrWeb
- Vim Script
- Visual Basic
- Visual Basic .NET
- wisp
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)
Coi: A type-safe, component-based language for building high-performance web apps with WASM and fine-grained reactivity.
Alternative interpretation of logical atomicity in Iris
Semantic Search & Call Graphs for AI Agents (100% Local)
Formalizing the stable marriage problem and the Gale-Shapley algorithm in Lean
Türkçe'ye daha yakın deneysel programlama dili / Experimental programming language closer to Turkish
Formalization of the proofs in the POPL 2026 paper Typing Strictness
The mechanized formalization of logical pinning, a lightweight borrowing model and proof discipline for precise reasoning about container-internal pointers.
Verifying a Lazy Concurrent List-Based Set Algorithm in Iris
Tampio: An object-oriented programming language made to resemble Finnish
Formalization of Vickrey-Clarke-Groves auction algorithm and mechanism (this repository is here for reference only; see mech.v for an up-to-date version)
The STM API we know and love, but useable in more circumstances
A bidirectional bindings generator for C++ and Rust.
In collaboration with the Rust Foundation, Rust Project, and appropriate external stakeholders, make C++ and Rust interoperability easily accessible and approachable to the widest possible audience
Specifications of the C++ standard library in BRiCk.
Financial Contracts eDSL & Valuation in Haskell. Final year dissertation project for my bachalors degree at University of Nottigham.