A proof assistant for higher-dimensional type theory

In-browser theorem-proving puzzle-game

A CLI for extracting libraries from Apple's dyld shared cache file

Demo for high-performance type theory elaboration

An experimental theorem prover

H.O.T.T. using rewriting in Agda

Used to generate and compare bounded timestamps.

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

A modern commutative diagram editor for the web.

Ocarina of Time trainer

Agda is a dependently typed programming language / interactive theorem prover.

Decompilation of The Legend of Zelda: Ocarina of Time

Experiments in formalizing and specifying computer systems with Agda

LaTeX-style mathematical symbols input method for macOS

Draft proposal for additional sub/superscript characters in Unicode

An open source re-implementation of RollerCoaster Tycoon 2 🎢

The Official Arduino AVR core

An experimental library for Cubical Agda

Non bloated asynchronous logger

Bare metal Raspberry Pi 3 tutorials

A modern proof language

BNF Converter

Metal I/O library for Rust.

A bare metal USB driver for Raspberry Pi 1-3 written in C

a brainfuck compiler written in brainfuck

Double-entry accounting system with a command-line reporting interface

Exam seating assignments

Petition to open source Flash and Shockwave spec

Web-based queue for office hours

agda-mode on Atom