agda/agda

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

Language: Haskell - Size: 148 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 2,698 - Forks: 380

the1lab/1lab

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

Language: Agda - Size: 9.67 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 393 - Forks: 84

agda/cornelis

agda-mode for neovim

Language: Haskell - Size: 12.1 MB - Last synced at: 2 days ago - Pushed at: about 1 month ago - Stars: 165 - Forks: 24

tree-sitter/tree-sitter-agda

Agda grammar for tree-sitter

Language: Yacc - Size: 31.1 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 37 - Forks: 16

jespercockx/agda-core

A work-in-progress core language for Agda, in Agda

Language: Agda - Size: 437 KB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 55 - Forks: 3

vehicle-lang/vehicle

A toolkit for enforcing logical specifications on neural networks

Language: Haskell - Size: 25 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 110 - Forks: 12

banacorn/agda-mode-vscode

agda-mode on VS Code

Language: ReScript - Size: 6.33 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 178 - Forks: 45

teach-types/www

MSc Course Types for Programs and Proofs (Chalmers DAT350 / GU DIT235)

Language: CSS - Size: 6.84 KB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 1 - Forks: 1

IntersectMBO/formal-ledger-specifications

Formal specifications of the Cardano ledger

Language: Agda - Size: 228 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 44 - Forks: 18

input-output-hk/iog-agda-prelude

Supplementary types and functions for the Agda prelude

Language: Agda - Size: 54.7 KB - Last synced at: 7 days ago - Pushed at: 8 days ago - Stars: 3 - Forks: 1

martinescardo/TypeTopology

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

Language: Agda - Size: 16.3 MB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 262 - Forks: 49

agda/cubical

An experimental library for Cubical Agda

Language: Agda - Size: 344 MB - Last synced at: 15 days ago - Pushed at: 15 days ago - Stars: 498 - Forks: 154

andreasabel/agda2lagda

Simple conversion from Agda text to literate Agda text.

Language: Haskell - Size: 163 KB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 14 - Forks: 0

awesomo4000/awesome-provable

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

Size: 25.4 KB - Last synced at: 10 days ago - Pushed at: over 3 years ago - Stars: 212 - Forks: 10

cdo256/virtualsets

Cubical investigation of sets with both negative and positive components

Language: Agda - Size: 426 KB - Last synced at: 24 days ago - Pushed at: 24 days ago - Stars: 0 - Forks: 0

gallais/agdarsec

Total Parser Combinators in Agda

Language: Agda - Size: 11.9 MB - Last synced at: 29 days ago - Pushed at: 29 days ago - Stars: 132 - Forks: 12

agda/agda-stdlib

The Agda standard library

Language: Agda - Size: 571 MB - Last synced at: 30 days ago - Pushed at: 30 days ago - Stars: 620 - Forks: 251

PHart3/2-groups-agda

A mechanized study of coherent 2-groups

Language: Agda - Size: 4.3 MB - Last synced at: about 6 hours ago - Pushed at: about 8 hours ago - Stars: 9 - Forks: 0

essentialblend/ms-thesis

Codebase for my MS thesis formalizing the commutative ring axioms of the integers in Agda

Language: Agda - Size: 30.3 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

zoedsoupe/paradigmas 📦

Experimentos e estudos, com base na cadeira de Paradigmas de Linguagens de Programação da UENF

Language: Racket - Size: 11.9 MB - Last synced at: 5 days ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

varikvalefor/mceliece

Language: Agda - Size: 960 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

HarrisonGrodin/agda-calf

A cost-aware logical framework, embedded in Agda.

Language: Agda - Size: 10.4 MB - Last synced at: 24 days ago - Pushed at: about 1 month ago - Stars: 64 - Forks: 4

agda/agda-language-server

Language Server for Agda

Language: Haskell - Size: 415 KB - Last synced at: 16 days ago - Pushed at: about 1 month ago - Stars: 113 - Forks: 18

ncfavier/agda-stuff

My Agda blog/lab/playground

Language: Agda - Size: 177 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 13 - Forks: 1

PHart3/Whitehead-agda

Proof of Whitehead's theorem for truncated types in Book HoTT

Language: Agda - Size: 14.1 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

xieyuheng/mugda

An implementation of the mugda paper

Language: TypeScript - Size: 2.99 MB - Last synced at: 17 days ago - Pushed at: about 2 months ago - Stars: 3 - Forks: 2

graded-type-theory/graded-type-theory

A Logical Relation for Martin-Löf Type Theory in Agda

Language: Agda - Size: 165 MB - Last synced at: 16 days ago - Pushed at: 16 days ago - Stars: 10 - Forks: 5

effectfully/inference-in-agda

A tutorial on how Agda infers things

Language: HTML - Size: 217 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 58 - Forks: 2

viercc/agda-container-plus

Applicative laws, presentation of container applicative

Language: Agda - Size: 158 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

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.

Language: HTML - Size: 80.9 MB - Last synced at: about 2 months ago - Pushed at: almost 4 years ago - Stars: 81 - Forks: 6

smimram/generated-deloopings-agda Fork of camilchp/generated-deloopings

Generated deloopings in Agda.

Language: Agda - Size: 155 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0

smimram/agda-polygraphs

Polygraphs in Agda.

Language: Agda - Size: 174 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 2 - Forks: 0

sourcedennis/docker-agda-mini

Small Docker images containing Agda

Language: Dockerfile - Size: 10.7 KB - Last synced at: 2 days ago - Pushed at: 2 months ago - Stars: 2 - Forks: 1

iblech/constructive-maximal-ideals

Reifying dynamical algebra: maximal ideals in countable rings, constructively

Language: TeX - Size: 5.34 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 4 - Forks: 0

choukh/agda-googology

formalized googology in agda

Language: CSS - Size: 3.72 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 2 - Forks: 0

jpvillaisaza/cain

Category theory applied to functional programming (undergraduate project)

Language: TeX - Size: 921 KB - Last synced at: 2 months ago - Pushed at: 4 months ago - Stars: 33 - Forks: 0

smimram/div2

An Agda formalization of "division by 2" in classical ZF without choice.

Language: Agda - Size: 3.05 MB - Last synced at: 3 months ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 0

felipeperet/logic Fork of rodrigogribeiro/logic

An adventure on formalizing logics using the Agda programming language

Language: Agda - Size: 59.6 KB - Last synced at: 6 days ago - Pushed at: almost 2 years ago - Stars: 10 - Forks: 2

essentialblend/integers-comm-ring

Type theoretical proofs in Agda proving the Ring of Integers.

Language: Agda - Size: 1.27 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

janheuer/here-and-there-agda

Implementation of the logic of here-and-there in Agda as the logical foundations of Answer Set Programming (ASP)

Language: Agda - Size: 229 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 3 - Forks: 0

gallais/agda-presburger

Deciding Presburger arithmetic in agda

Language: Agda - Size: 155 KB - Last synced at: 3 months ago - Pushed at: over 2 years ago - Stars: 32 - Forks: 3

agda/agda-pkg

apkg - package manager for Agda

Language: Python - Size: 19 MB - Last synced at: 16 days ago - Pushed at: about 4 years ago - Stars: 38 - Forks: 8

ixaxaar/monoid.space

Learn pure math with agda :rocket:

Language: HTML - Size: 11.3 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 17 - Forks: 0

phijor/cubical-containers

Language: Agda - Size: 536 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 5 - Forks: 0

owsky/AgdaHeap

Heap data structure implemented with Agda

Language: Agda - Size: 42 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

martinescardo/HoTT-UF-Agda-Lecture-Notes

Lecture notes on univalent foundations of mathematics with Agda

Language: Agda - Size: 5.8 MB - Last synced at: 4 months ago - Pushed at: over 1 year ago - Stars: 227 - Forks: 20

4e554c4c/blink-cmp-agda-symbols

Agda symbols source for the blink.cmp neovim completion engine

Language: Lua - Size: 78.1 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

jonaprieto/agda-prop 📦

A Library for Classical Propositional Logic in Agda

Language: Agda - Size: 442 KB - Last synced at: about 2 months ago - Pushed at: almost 6 years ago - Stars: 16 - Forks: 1

teach-afp/www

Public webpage for the course AFP (Advanced Functional Programming)

Language: HTML - Size: 21.5 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 1

alan-j-hu/camyll

Static site generator

Language: OCaml - Size: 208 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 11 - Forks: 1

juniorxxue/contextual-typing

Contextual Typing, formalized in Agda

Language: Agda - Size: 3.64 MB - Last synced at: 3 days ago - Pushed at: 7 months ago - Stars: 9 - Forks: 0

Gradual-Typing/LambdaIFCStar

The Agda mechanization of a gradual security-typed programming language with general mutable references.

Language: Agda - Size: 971 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 4 - Forks: 1

pthariensflame/agda-fumulas

An exploration of fumulas in Agda—a new perspective on ring theory

Language: Agda - Size: 185 KB - Last synced at: 1 day ago - Pushed at: 5 months ago - Stars: 2 - Forks: 0

HoTT/HoTT-Agda

Development of homotopy type theory in Agda

Language: Agda - Size: 6.15 MB - Last synced at: 5 months ago - Pushed at: over 6 years ago - Stars: 424 - Forks: 58

EgbertRijke/HoTT-Intro 📦

An introductory course to Homotopy Type Theory

Language: Agda - Size: 7.11 MB - Last synced at: 5 months ago - Pushed at: about 5 years ago - Stars: 365 - Forks: 28

alhassy/gentle-intro-to-reflection

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

Language: Agda - Size: 57.6 KB - Last synced at: 4 months ago - Pushed at: over 3 years ago - Stars: 101 - Forks: 9

freeman42x/blog

Software engineering and artificial general intelligence blog of Răzvan Flavius Panda

Size: 37.1 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 17 - Forks: 2

smimram/fibred-polynomials

Formalizing polynomials in groupoids.

Language: Agda - Size: 63.5 KB - Last synced at: 5 months ago - Pushed at: over 2 years ago - Stars: 8 - Forks: 1

isovector/certainty-by-construction

Source material for Certainty by Construction

Language: TeX - Size: 7.46 MB - Last synced at: 5 months ago - Pushed at: over 1 year ago - Stars: 41 - Forks: 12

gallais/generic-syntax

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

Language: Agda - Size: 10.6 MB - Last synced at: 5 months ago - Pushed at: over 3 years ago - Stars: 72 - Forks: 11

juniorxxue/system-f

System F in Agda with well-scoped de Bruijn indices

Language: Agda - Size: 4.88 KB - Last synced at: 3 days ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

xgrommx/agda-ecosystem

Size: 31.3 KB - Last synced at: 5 months ago - Pushed at: over 7 years ago - Stars: 30 - Forks: 1

4e554c4c/agda-symbols

A machine-readible list of unicode symbols used for writing Agda

Size: 28.3 KB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0

ualib/agda-algebras

The Agda Universal Algebra Library (html docs available at the url below)

Language: Agda - Size: 65 MB - Last synced at: 5 months ago - Pushed at: 9 months ago - Stars: 33 - Forks: 7

konstantinosKokos/quill

🪶 Neural premise selection for Agda.

Language: Python - Size: 3.33 MB - Last synced at: 6 months ago - Pushed at: 8 months ago - Stars: 2 - Forks: 0

wolverian/agda-template

A template for an Agda project with automatic GitHub Pages support

Language: CSS - Size: 2.44 MB - Last synced at: 3 days ago - Pushed at: over 2 years ago - Stars: 8 - Forks: 1

wenkokke/schmitty

Agda bindings to SMT-LIB2 compatible solvers.

Language: Agda - Size: 9.79 MB - Last synced at: 6 months ago - Pushed at: 11 months ago - Stars: 96 - Forks: 8

hazelgrove/hazelnut-livelits-agda

mechanization for livelits paper, https://github.com/hazelgrove/livelits-paper

Language: Agda - Size: 585 KB - Last synced at: 6 months ago - Pushed at: over 4 years ago - Stars: 6 - Forks: 0

alhassy/AgdaCheatSheet

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

Language: Agda - Size: 460 KB - Last synced at: 4 months ago - Pushed at: over 3 years ago - Stars: 39 - Forks: 1

ggzor/specifying-verifying-tail-recursion

Source code for the paper "Specifying and Verifying a Transformation of Recursive Functions into Tail-Recursive Functions"

Language: TeX - Size: 2.5 MB - Last synced at: 4 days ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 1

brendanzab/agda-logic-playground

Messing around with propositional logic in Agda

Language: Agda - Size: 1.95 KB - Last synced at: 3 months ago - Pushed at: almost 9 years ago - Stars: 1 - Forks: 0

vendethiel/dependent-printf

I'm terrible at this, eh.

Language: Agda - Size: 109 KB - Last synced at: 2 months ago - Pushed at: about 11 years ago - Stars: 1 - Forks: 0

andreasabel/red-black-tree-left-leaning

Left-leaning red-black trees in Agda (insertion and deletion) with static ordering and balancing invariants

Language: Agda - Size: 151 KB - Last synced at: 3 months ago - Pushed at: 7 months ago - Stars: 2 - Forks: 0

bracevac/dotter

Towards richer dependent types for DOT

Language: Coq - Size: 365 KB - Last synced at: 5 months ago - Pushed at: over 4 years ago - Stars: 5 - Forks: 0

scott-fleischman/agda-from-nothing

A workshop on learning Agda with minimal prerequisites.

Language: Agda - Size: 422 KB - Last synced at: 5 months ago - Pushed at: over 9 years ago - Stars: 85 - Forks: 6

ilya-klyuchnikov/ttlite

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

Language: Scala - Size: 1.5 MB - Last synced at: 5 months ago - Pushed at: over 3 years ago - Stars: 120 - Forks: 9

vikraman/2DTypes

Collaborative work on reversible computing

Language: TeX - Size: 42.3 MB - Last synced at: 6 months ago - Pushed at: about 3 years ago - Stars: 18 - Forks: 1

t-wissmann/Initial-Algebras-Unchained

Mirror of https://git8.cs.fau.de/software/initial-algebras-unchained

Language: Agda - Size: 350 KB - Last synced at: 5 days ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 0

TOTBWF/cubical-categories

Category theory formalized in cubical agda

Language: Agda - Size: 37.1 KB - Last synced at: 6 months ago - Pushed at: over 5 years ago - Stars: 20 - Forks: 0

jonaprieto/agda-metis

Metis Prover Reasoning for Propositional Logic in Agda

Language: Agda - Size: 765 KB - Last synced at: 3 months ago - Pushed at: almost 7 years ago - Stars: 2 - Forks: 1

algebraic-graphs/agda

The theory of algebraic graphs formalised in Agda

Language: Agda - Size: 42 KB - Last synced at: 4 months ago - Pushed at: about 7 years ago - Stars: 89 - Forks: 6

keilambda/ttfpi-agda

Formalization of the book "Type Theory and Formal Proof: An Introduction" in Agda

Language: Agda - Size: 60.5 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 3 - Forks: 0

leo-leesco/Computational-Logic-TD7

Sorting

Language: Agda - Size: 10.7 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 0 - Forks: 0

langston-barrett/write-yourself-a-scheme-in-agda 📦

Like "Write Yourself a Scheme in 48 Hours", but in Agda

Language: Agda - Size: 66.4 KB - Last synced at: 5 months ago - Pushed at: over 7 years ago - Stars: 52 - Forks: 2

akiomik/plfa-solutions

Solutions for PLFA (Programming Language Foundations in Agda) exercise

Language: Agda - Size: 122 KB - Last synced at: 5 months ago - Pushed at: almost 4 years ago - Stars: 8 - Forks: 0

gergoerdi/stlc-agda

STLC-related snippets in Agda

Size: 164 KB - Last synced at: 6 months ago - Pushed at: over 12 years ago - Stars: 16 - Forks: 1

alhassy/org-agda-mode

An Emacs mode for working with Agda code in an Org-mode like fashion, more or less.

Language: Emacs Lisp - Size: 85.9 KB - Last synced at: 5 months ago - Pushed at: almost 4 years ago - Stars: 18 - Forks: 7

lemastero/agda-smash

smash product in Agda

Language: Agda - Size: 85.9 KB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 0 - Forks: 0

hauntedhost/programming-language-foundations-in-agda

Programming Language Foundations in Agda by Philip Wadler and Wen Kokke

Language: Agda - Size: 257 KB - Last synced at: about 1 month ago - Pushed at: 9 months ago - Stars: 0 - Forks: 0

giorgiosld/Static-Analysis-and-Program-Verification 📦

This repo contains the material about the course "Static Analysis and Program Verification" supplied in the Master Degree (LM-18) at the University of Camerino

Language: Agda - Size: 876 KB - Last synced at: 4 months ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

williamdemeo/agda-algebras Fork of ualib/agda-algebras

The Agda Universal Algebra Library (html docs available at the url below)

Language: Agda - Size: 54.5 MB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 1 - Forks: 1

jpvillaisaza/abel

Category theory applied to functional programming

Language: Agda - Size: 80.1 KB - Last synced at: 4 months ago - Pushed at: about 9 years ago - Stars: 7 - Forks: 0

Seeker04/stlc-agda-elab

Agda formalisation of an elaborator for a simply typed language

Language: Agda - Size: 4.98 MB - Last synced at: 6 months ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

lane-core/kitcat

Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda

Language: Agda - Size: 134 KB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 5 - Forks: 0

RiscadoA/class-agda-playground

An incomplete implementation of CLASS's type system in Agda

Language: Agda - Size: 7.81 KB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 3 - Forks: 0

jespercockx/ataca

A TACtic library for Agda

Language: Agda - Size: 48.8 KB - Last synced at: 2 months ago - Pushed at: 12 months ago - Stars: 48 - Forks: 4

scott-fleischman/greek-grammar

Modeling Ancient Greek Grammar

Language: Agda - Size: 311 MB - Last synced at: 5 months ago - Pushed at: over 7 years ago - Stars: 50 - Forks: 7

m0rphism/kitty

An Agda Framework for programming language metatheory based on extrinsic typing, intrinsic scoping and de Bruijn indices.

Language: Agda - Size: 1.85 MB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 1 - Forks: 0

sstucki/f-omega-int-agda

F-omega with interval kinds mechanized in Agda

Language: Agda - Size: 448 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 13 - Forks: 3

iwilare/church-rosser

A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses the infrastructure for λ-terms and substitutions provided by the PLFA book

Language: Agda - Size: 70.3 KB - Last synced at: about 1 year ago - Pushed at: almost 3 years ago - Stars: 22 - Forks: 1