agda
There are 261 repositories under agda topic.
agda/agda
Agda is a dependently typed programming language / interactive theorem prover.
agda/agda-stdlib
The Agda standard library
agda/cubical
An experimental library for Cubical Agda
HoTT/HoTT-Agda
Development of homotopy type theory in Agda
EgbertRijke/HoTT-Intro
An introductory course to Homotopy Type Theory
the1lab/1lab
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
martinescardo/TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
martinescardo/HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
awesomo4000/awesome-provable
A curated set of links to formal methods involving provable code.
banacorn/agda-mode-vscode
agda-mode on VS Code
copumpkin/categories
Categories parametrized by morphism equality, in Agda
isovector/cornelis
agda-mode for neovim
gallais/agdarsec
Total Parser Combinators in Agda
HoTT-Intro/Agda
Agda formalisation of the Introduction to Homotopy Type Theory
ilya-klyuchnikov/ttlite
A SuperCompiler for Martin-Löf's Type Theory
agda/agda-language-server
Language Server for Agda
wenkokke/schmitty
Agda bindings to SMT-LIB2 compatible solvers.
alhassy/gentle-intro-to-reflection
A slow-paced introduction to reflection in Agda. ---Tactics!
algebraic-graphs/agda
The theory of algebraic graphs formalised in Agda
scott-fleischman/agda-from-nothing
A workshop on learning Agda with minimal prerequisites.
alhassy/next-700-module-systems
PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.
vehicle-lang/vehicle
A toolkit for enforcing logical specifications on neural networks
gallais/generic-syntax
A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
banacorn/agda-mode
agda-mode on Atom
fredefox/cat
A formalization of category theory in cubical Agda
jonsterling/agda-calf
A cost-aware logical framework, embedded in Agda.
langston-barrett/write-yourself-a-scheme-in-agda
Like "Write Yourself a Scheme in 48 Hours", but in Agda
scott-fleischman/greek-grammar
Modeling Ancient Greek Grammar
jespercockx/ataca
A TACtic library for Agda
mr-ohman/logrel-mltt
A Logical Relation for Martin-Löf Type Theory in Agda
wenkokke/AutoInAgda
Proof automation – for Agda, in Agda.
agda/agda-pkg
apkg - package manager for Agda
oisdk/agda-ring-solver
A fast, easy-to-use ring solver for agda with step-by-step solutions
alhassy/AgdaCheatSheet
Basics of the dependently-typed functional language Agda ^_^
IntersectMBO/formal-ledger-specifications
Formal specifications of the cardano ledger
isovector/certainty-by-construction
Source material for Certainty by Construction