Agda Open Source Projects

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

A collection of resources for learning type theory and type theory adjacent fields.

An introduction to programming language theory in Agda

The Agda standard library

BNF Converter

Demo for high-performance type theory elaboration

An experimental library for Cubical Agda

Development of homotopy type theory in Agda

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

A new Categories library for Agda

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

An introductory course to Homotopy Type Theory

A course on homotopy theory and type theory, taught jointly with Jaka Smrekar

The agda-unimath library

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

being the lecture materials and exercises for the 2017/18 session of CS410 Advanced Functional Programming at the University of Strathclyde

An in-progress fast, dependently typed, functional programming language implemented in Swift.

Lecture notes on univalent foundations of mathematics with Agda

A curated set of links to formal methods involving provable code.

《编程语言基础：Agda 描述》，Programming Language Foundations in Agda 中文版

Compiling Agda code to readable Haskell

agda-mode on VS Code

agda-mode for neovim

Categories parametrized by morphism equality, in Agda

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

My slides and notes

Agda interaction in vim

Total Parser Combinators in Agda

REST'ful web framework in Agda

A toolkit for enforcing logical specifications on neural networks

Agda formalisation of the Introduction to Homotopy Type Theory

Language Server for Agda

A SuperCompiler for Martin-Löf's Type Theory

Awesome List of my own!

Agda bindings to SMT-LIB2 compatible solvers.

A slow-paced introduction to reflection in Agda. ---Tactics!

ECMAScript back end for Functional Reactive Programming in Agda