Category theory in Rocq

Org-mode to Typst exporter.

Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

Unofficial EPFL beamer template.

An itree-like data-structure to additionally support internal non-determinism

A Library for Representing Recursive and Impure Programs in Coq

Formally verified operator language and rewriting engine for high-performance computing

OCaml as a Tactic Language for the Rocq Prover

The Vellvm (Verified LLVM) coq development.

org-mode modules for citations, cross-references, bibliographies in org-mode and useful bibtex tools to go with it.

Moloch is a minimalist, feature-rich Beamer theme for LaTeX presentations with a clean design and extensive customization options.

🍃 SimplePlus - A minimalist and clean LaTeX Beamer theme

A modern LaTeX Beamer theme

Simple, typographic beamer theme

A Rust verification tool

A foundational framework for modular cryptographic proofs in Coq

Shrinking induction-recursion... sometimes you just wanna be small!

coinduction library for Coq

An extremely fast Python package and project manager, written in Rust.

A formal development of constructive domain theory in Coq

Malloc / Free / Realloc / Calloc implementation using a red-black tree

Gallina to Bedrock2 compilation toolkit

Bump allocator in C

Reimplementing malloc(), calloc(), realloc(), free() in c from scratch using system calls

Language for high-assurance and high-speed cryptography

Named overlays for Beamer

Mechanized baselines for various type system features

An axiom-free formalization of category theory in Coq for personal study and practical work