Demo for high-performance type theory elaboration

Staged compilation with dependent types

A formalization of the polymorphic lambda calculus extended with iso-recursive types

System F-omega normalization by hereditary substitution in Agda

A Lean4 Formalization of Polynomial Functors

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

An evaluation benchmark for undergraduate competition math in Lean4, Isabelle, Coq, and natural language.

A formally verified interpreter for Lambda Calculus.

A LaTeX template for Bachelor or Master theses

Learn Lean 4 with PLFA proofs.

Lean documentation authoring tool

Personal web site for Yoo Chung.

Miller–Rabin primality test in Lean

Topos theory in lean

SampCert : Verified Differential Privacy

An interactive theorem prover for string diagrams

My C# .NET solution to the Synacor OSCON 2012 Challenge

Hakyll + Nix starter template

Work with Celeste files in Rust!

A library for probabilistic programming in Haskell.

✨ Programming Language Research, Applied PLT & Compilers

Temporary repository for Kind2's refactor based on HVM2

LaTeX dissertation template and examples for a Ph.D. in Physics at Drexel

Formalized laws for mtl

Formalization of the polymorphic lambda calculus and its parametricity theorem

buffon's needle in lean 4

Formalized quantum computing in Lean theorem prover

The matrix cookbook, proved in the Lean theorem prover