Lists (32)
📽 Animation
5 repositories
🖼️ Art
3 repositories
📜 Binary Formats
54 repositories
🌀 Bootstrapping
49 repositories
🏗️ Build systems
13 repositories
📝 Compilation
32 repositories
🎨 Creative Tools
38 repositories
🗄 Data Layout
3 repositories
🌱 Digital Gardens - Examples
10 repositories
🌱 Digital Gardens - Tools
42 repositories
📖 Documentation - Tools
3 repositories
🚀 Effects
Effect systems, Algebraic effects and handlers… resources, languages, libraries and use cases58 repositories
🗣 Elaboration
Examples of elaborating surface languages into minimal core languages26 repositories
🐟 Fish Shell
4 repositories
🔠 Fonts
28 repositories
🕹️ Game Development
3 repositories
🕹️ Games
2 repositories
📐 Geometric Algebra
18 repositories
👍 Memory Safe by Default
4 repositories
🍱 Module Systems - Case Studies
3 repositories
🍱 Module Systems - Languages
12 repositories
🏡 My Stack
14 repositories
⚙️ Nix - Example Configurations
12 repositories
⚙️ Nix - Tools
37 repositories
💾 Nostalgia
29 repositories
🐪 OCaml - js_of_ocaml
3 repositories
🏔 Procedural
Things related to procedural generation, generated worlds, etc.57 repositories
🎲 Property Based Testing
4 repositories
🖼 Shaders
16 repositories
⏱ Staged Programming
8 repositories
🌳 Structural Editing
14 repositories
🏔 World Building - Conlanging
8 repositories
Starred repositories
135
stars
written in Coq
Clear filter
The CompCert formally-verified C compiler
Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
Cryptographic Primitive Code Generation by Fiat
An axiom-free formalization of category theory in Coq for personal study and practical work
A framework for formally verifying distributed systems implementations in Coq
Tricks you wish the Coq manual told you [maintainer=@tchajed]
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
A Learning Environment for Theorem Proving with the Coq proof assistant
Language for high-assurance and high-speed cryptography
A work-in-progress language and compiler for verified low-level programming
My personal repository of formally verified mathematics.
Randomized Property-Based Testing Plugin for Coq
A Library for Representing Recursive and Impure Programs in Coq
Mathematical Components compliant Analysis Library
A function definition package for Rocq
Formal proof of the Four Color Theorem [maintainer=@ybertot]
Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older versio…
A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
Proofs in Coq for the book Reflective Programs in Tree Calculus
Lecture notes for a short course on proving/programming in Coq via SSReflect.
A core language for rule-based hardware design 🦑
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
A Verified Compiler for Gallina, Written in Gallina