Lists (32)
3D print related
AIGC
airport
automatica
C++ lib
chromebook
compiler stuff
cpython
debugger
ELEC
font
formal
🔮 Future ideas
game
gh
graphics
gui
hardware
HPC
image ai
ios
learn
Mathlib
net lib
radio
riscv
texocr
texocrs
typst
video process
VM
wasm
Stars
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
Randomized Property-Based Testing Plugin for Coq
A formalization of geometry in Coq based on Tarski's axiom system
A Verified Compiler for Gallina, Written in Gallina
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
My solutions to Software Foundations course in Coq proof assistant.
Some unstructured notes concerning the Broad tutorial to take place in March 2020
Formalization of Axiomatic Set Theory in Coq
Formally verified numerical integration of an ordinary differential equation
A Coq tactic for proving multivariate inequalities using SDP solvers
VST verification of programs from the cbench benchmark
Translation of HOL-Light's Multivariate library in Rocq