agda

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

The Agda standard library

Development of homotopy type theory in Agda

An introductory course to Homotopy Type Theory

Lecture notes on univalent foundations of mathematics with Agda

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

Categories parametrized by morphism equality, in Agda

🌀 Configuration-free text editor limited to VT100. Suitable for writing git commit messages, editing Markdown, config files, source code, viewing man pages and for quick edit-compile cycles when programming. Includes syntax highlighting, quick compilation and formatting, jump-to-error, rainbow parenthesis, tab completion, smart indentation, macros and cut/paste portals.

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

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

agda-mode on VS Code

Agda formalisation of the Introduction to Homotopy Type Theory

Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.

Total Parser Combinators in Agda

A workshop on learning Agda with minimal prerequisites.

Agda bindings to SMT-LIB2 compatible solvers.

PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.

The theory of algebraic graphs formalised in Agda

Language Server for Agda

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

agda-mode on Atom

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

Univalent mathematics in Agda

A formalization of category theory in cubical Agda

A TACtic library for Agda

Modeling Ancient Greek Grammar

agda-mode for neovim

A fast, easy-to-use ring solver for agda with step-by-step solutions

Proof automation – for Agda, in Agda.

Basics of the dependently-typed functional language Agda ^_^