Lean 3 material for Kevin Buzzard's Jan-Mar 2022 course on formalising mathematics. Lean 4 version available here: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024

Describe Toki Pona using Grammatical Framework

C11 compiler (mirror)

Flight rules for git

Automatic test case generation for GF grammars

Grammatical Framework's Resource Grammar Library (RGL)

Grammatical Framework core: compiler, shell & runtimes

Generating test cases for GF grammars

A major mode for editing GF code.

All CPU and MCU documentation in one place

A sunny little virtual machine

TinyVM is a small, fast, lightweight virtual machine written in pure ANSI C.

This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

Experimental implementation of Cubical Type Theory

Development of homotopy type theory in Agda

What I Wish I Knew When Learning Haskell

A portable foreign-function interface library.

Community contributions to the Grammatical Framework

Archive of monolithic GF repository until 2018-07-25

Example OpenRISC backend