Skip to content
View brendanzab's full-sized avatar
πŸ˜΅β€πŸ’«
writing elaborators
πŸ˜΅β€πŸ’«
writing elaborators

Sponsoring

@servo

Organizations

@yeslogic @rust-lang @PistonDevelopers @gluon-lang @proglangdesign @pikelet-lang

Block or report brendanzab

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse

πŸ“½ Animation

5 repositories

πŸ–ΌοΈ Art

3 repositories

πŸ“œ Binary Formats

53 repositories

πŸŒ€ Bootstrapping

47 repositories

πŸ—οΈ Build systems

11 repositories

πŸ“ Compilation

29 repositories

🎨 Creative Tools

36 repositories

πŸ—„ Data Layout

3 repositories

Starred repositories

134 stars written in Agda
Clear filter

An introduction to programming language theory in Agda

Agda 1,449 338 Updated Jul 27, 2025

The Agda standard library

Agda 620 251 Updated Aug 6, 2025

An experimental library for Cubical Agda

Agda 498 154 Updated Aug 4, 2025

Development of homotopy type theory in Agda

Agda 430 58 Updated Feb 19, 2019

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

Agda 388 81 Updated Aug 10, 2025

A new Categories library for Agda

Agda 384 71 Updated Aug 3, 2025

Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations

Agda 381 27 Updated Oct 23, 2023

An introductory course to Homotopy Type Theory

Agda 373 29 Updated Jul 24, 2020

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

Agda 262 49 Updated Aug 8, 2025

The agda-unimath library

Agda 261 84 Updated Aug 9, 2025

Lecture notes on univalent foundations of mathematics with Agda

Agda 229 20 Updated Apr 16, 2024

Compiling Agda code to readable Haskell

Agda 190 42 Updated Jul 30, 2025

Categories parametrized by morphism equality, in Agda

Agda 151 24 Updated Aug 9, 2019

Total Parser Combinators in Agda

Agda 132 12 Updated Aug 5, 2025

Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT

Agda 130 17 Updated Apr 9, 2024

Programming library for Agda

Agda 130 24 Updated Aug 22, 2024

Agda formalisation of the Introduction to Homotopy Type Theory

Agda 125 4 Updated Nov 27, 2021

Agda bindings to SMT-LIB2 compatible solvers.

Agda 101 8 Updated Oct 7, 2024

The theory of algebraic graphs formalised in Agda

Agda 90 6 Updated Jul 15, 2018

A workshop on learning Agda with minimal prerequisites.

Agda 86 6 Updated May 26, 2016

Algebra of Programming in Agda: Dependent Types for Relational Program Derivation

Agda 83 9 Updated Jul 11, 2016

Abstract binding trees (abstract syntax trees plus binders), as a library in Agda

Agda 75 5 Updated Jul 30, 2025

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

Agda 75 11 Updated Mar 5, 2022

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

Agda 71 8 Updated May 10, 2019

Inline, type safe X86-64 assembly programming in Agda

Agda 70 2 Updated Jan 3, 2019

Summer school on programming in Agda

Agda 68 15 Updated Aug 1, 2023

Miller/pattern unification in Agda

Agda 65 1 Updated Feb 6, 2014

A cost-aware logical framework, embedded in Agda.

Agda 64 4 Updated Jul 27, 2025

This aims to be the most pretentious implementation of stlc in existence

Agda 63 2 Updated Mar 5, 2022

Learn the Agda basics in three 2-hour sessions.

Agda 60 7 Updated Oct 24, 2023
Next