Fine-grained parallelism with sub-nanosecond overhead in Zig

RISC-V Specification in Coq

A FUSE filesystem for your Google calendar

Neovim :: M Λ C R O - Editing made simple

Visual Studio Code Extension and Language Server Protocol for Coq

Neovim client for coq-lsp

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

Tricks you wish the Coq manual told you [maintainer=@tchajed]

We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

A Neovim client for VsCoq 2 vscoqtop.

A lightweight library for portable low-level GPU computation using WebGPU.

Haskell bindings to libcmark-gfm GitHub Flavored Markdown parser

Delightful io_uring packages and resources

Portable interface to epoll, kqueue, event ports, and wepoll

Dynamic Tracing in Linux

AeroSpace is an i3-like tiling window manager for macOS

The Paxos library implemented in C++ that has been used in the WeChat production environment.

An embedded, in-memory, zero-copy, atomicity, consistency, isolation, MVCC, almost lock-free and serializable snapshot isolation database engine.

TPP experimentation on MLIR for linear algebra

A Go unikernel running on x86 bare metal

Hermit for Rust.

A kernel designed to run one and only one application in a virtualized environment

The reference implementation of the Linux FUSE (Filesystem in Userspace) interface

The rustic MLIR bindings in Rust

Formal Reasoning About Programs

A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]

LLRT (Low Latency Runtime) is an experimental, lightweight JavaScript runtime designed to address the growing demand for fast and efficient Serverless applications.

C/C++ frontend for MLIR. Also features polyhedral optimizations, parallel optimizations, and more!

Coq development for the course "Mechanized semantics", Collège de France, 2019-2020