#
Lists (32)
📽 Animation
5 repositories
🖼️ Art
3 repositories
📜 Binary Formats
55 repositories
🌀 Bootstrapping
48 repositories
🏗️ Build systems
11 repositories
📝 Compilation
29 repositories
🎨 Creative Tools
36 repositories
🗄 Data Layout
3 repositories
🌱 Digital Gardens - Examples
9 repositories
🌱 Digital Gardens - Tools
41 repositories
📖 Documentation - Tools
3 repositories
🚀 Effects
Effect systems, Algebraic effects and handlers… resources, languages, libraries and use cases53 repositories
🗣 Elaboration
Examples of elaborating surface languages into minimal core languages25 repositories
🐟 Fish Shell
4 repositories
🔠 Fonts
27 repositories
🕹️ Game Development
2 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
34 repositories
💾 Nostalgia
28 repositories
🐪 OCaml - js_of_ocaml
3 repositories
🏔 Procedural
Things related to procedural generation, generated worlds, etc.52 repositories
🎲 Property Based Testing
4 repositories
🖼 Shaders
16 repositories
⏱ Staged Programming
6 repositories
🌳 Structural Editing
14 repositories
🏔 World Building - Conlanging
8 repositories
Starred repositories
135
stars
written in Coq
Clear filter
Mostly Automated Synthesis of Correct-by-Construction Programs
A Verified Compiler for Gallina, Written in Gallina
Advent of Code 2018, in Coq! (https://adventofcode.com/2018)
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Formal specification and verification of hardware, especially for security and privacy.
A framework for smart contract verification in Coq
A library of mechanised undecidability proofs in the Coq proof assistant.
A mechanisation of Wasm in Coq(Rocq)
High level commands to declare a hierarchy based on packed classes
Formalising Type Theory in a modular way for translations between type theories
A formally verified high-level synthesis tool based on CompCert and written in Coq.
Collapsing Towers of Interpreters
Formalization of Machine Learning Theory with Applications to Program Synthesis
Monadic effects and equational reasoning in Rocq
A formalisation of the Calculus of Constructions
Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
Formalization of the Dependent Object Types (DOT) calculus
A Specification for Dependent Types in Haskell (Core)
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]