Minimal implementations for dependent type checking and elaboration

Wasm Analysis Framework For Lightweight Experiments

Website for CS 265

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

Strongly-typed System F in Haskell

Malfunctional Programming

Formalization of CBPV extended with effect and coeffect tracking

LaTeX code for a paper on lean's type theory

A proof assistant and a dependently-typed language

A Specification for Dependent Types in Haskell (Core)

FunTAL: mixing a functional language with assembly.

A demo implementation of a simple dependently-typed language

Files for cross-compilation

Implementations of various type systems in OCaml.

A functional programming language with shell scripting capabilities

A dependently typed programming language with direct style effects and linearity

A Framework for building Batched Concurrent Data Structures

Concurrency Primer

Code auditing productivity multiplier.

A Model Sharded Key-Value Store Implementation using Go and Kubernetes.

Magical Deterministic Simulator for distributed systems in Rust.

A modern supercompiler for call-by-value functional languages

Resources for Learning PLT Redex

A high-performance, parallel, compilation-based symbolic execution engine

Hosts the website for mathlib and other Lean community infrastructure.

a model of MIR and the Rust type/trait system

Overview of tactics in Lean 4 for beginners — longer version