An annotated implementation of the Transformer paper.

A menagerie of cute implementations of modern typechecking algorithms

An experimental proof assistant based on a type theory for synthetic ∞-categories.

How to build an increasingly complex C/C++ codebase to WebAssembly

The Twelf Programming Language

ITT 1979 in Twelf (à la Constructive Mathematics and Computer Programming)

modular development of intensional type theory in twelf

Proofs for type systems and logical systems in Twelf

Twelf Tutorial and Twelf Encoding of Minilang

Library classes for the Twelf Proof System

Haskell implementation of the Edinburgh Logical Framework

Logical manifestations of topological concepts, and other things, via the univalent point of view.

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

A gently curated list of companies using verification formal methods in industry

Master programming by recreating your favorite technologies from scratch.

The missing bridge between Java and native C++

Example of using C++ classes from Java. Showcases SWIG, JNA and JNI

A textbook on informal homotopy type theory

Quantomatic is a tool for doing automated graph rewriting.

Selected Papers of Dana S. Scott

A demo implementation of a simple dependently-typed language

A modern LaTeX Beamer theme

Learn the Agda basics in three 2-hour sessions.

Script to download all of Hackage

Blog post previews in need of peer review

A curated list of amazingly awesome Haskell articles and talks for beginners.

Free Client for OneDrive on Linux

A prototypical dependently typed languages with sized types and variances

Converts Microsoft Word docx to LaTeX