Monads are not just monoids in the category of endofunctors.

Derive DecidableEq instances for nested mutual inductives

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.

The Hitchhiker's Guide to Logical Verification (2026 edition) and associated materials

An awesome list of e-graph resources

Versatile typeface for code, from code.

A mechanisation of Wasm in Isabelle.

Quickly rewrite git repository history (filter-branch replacement)

A slow-paced introduction to reflection in Agda. ---Tactics!

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

A free (as in freedom) OCaml textbook

Wasm SpecTec specification tools

A collection of resources for learning type theory and type theory adjacent fields.

A programming language supporting most features of both declarative and imperative languages

Mechanizations of Type Theories

Repository for the book "Crafting Interpreters"

Type Theory

A gentle introduction to Isabelle and Isabelle/HOL

A general map auto annotation framework based on MapTR, with high flexibility in terms of spatial scale and element type

[ECCV 2022 Oral] OpenLane: Large-scale Realistic 3D Lane Dataset

[NeurIPS 2023 Track Datasets and Benchmarks] OpenLane-V2: The First Perception and Reasoning Benchmark for Road Driving

Contrastive unpaired image-to-image translation, faster and lighter training than cyclegan (ECCV 2020, in PyTorch)

Image-to-Image Translation in PyTorch

A garden of small programming language implementations 🪴

Vision-Centric BEV Perception: A Survey

Automatic driving long tail / corner cases scenarios dataset (Anomaly detection)

PyTorch implementation of the U-Net for image semantic segmentation with high quality images

mawww's experiment for a better code editor

Dilated Residual Networks