agda/agda-stdlib

The Agda standard library

Language: Agda - Size: 550 MB - Last synced at: about 8 hours ago - Pushed at: about 9 hours ago - Stars: 610 - Forks: 247

input-output-hk/iog-agda-prelude

Supplementary types and functions for the Agda prelude

Language: Agda - Size: 47.9 KB - Last synced at: about 8 hours ago - Pushed at: 7 days ago - Stars: 2 - Forks: 0

ncfavier/cubical-experiments

Experiments with Cubical Agda

Language: Agda - Size: 163 KB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 9 - Forks: 1

agda/agda

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

Language: Haskell - Size: 146 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 2,614 - Forks: 368

the1lab/1lab

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

Language: Agda - Size: 8.75 MB - Last synced at: 2 days ago - Pushed at: 3 days ago - Stars: 366 - Forks: 72

4e554c4c/blink-cmp-agda-symbols

Agda symbols source for the blink.cmp neovim completion engine

Language: Lua - Size: 78.1 KB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 0 - Forks: 0

IntersectMBO/formal-ledger-specifications

Formal specifications of the cardano ledger

Language: Agda - Size: 187 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 40 - Forks: 16

PHart3/2-groups-agda

Mechanized study of coherent 2-groups

Language: Agda - Size: 709 KB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 1 - Forks: 0

agda/cubical

An experimental library for Cubical Agda

Language: Agda - Size: 313 MB - Last synced at: 10 days ago - Pushed at: about 1 month ago - Stars: 477 - Forks: 145

graded-type-theory/graded-type-theory

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

Language: Agda - Size: 151 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 7 - Forks: 5

martinescardo/TypeTopology

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

Language: Agda - Size: 17.6 MB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 253 - Forks: 45

awesomo4000/awesome-provable

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

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

teach-afp/www

Public webpage for the course AFP (Advanced Functional Programming)

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

vehicle-lang/vehicle

A toolkit for enforcing logical specifications on neural networks

Language: Haskell - Size: 23.9 MB - Last synced at: 10 days ago - Pushed at: 14 days ago - Stars: 87 - Forks: 10

alan-j-hu/camyll

Static site generator

Language: OCaml - Size: 208 KB - Last synced at: 15 days ago - Pushed at: 15 days 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: 2 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: 16 days ago - Pushed at: 16 days ago - Stars: 4 - Forks: 1

agda/cornelis

agda-mode for neovim

Language: Haskell - Size: 12.1 MB - Last synced at: 7 days ago - Pushed at: 21 days ago - Stars: 150 - Forks: 24

banacorn/agda-mode-vscode

agda-mode on VS Code

Language: ReScript - Size: 4.75 MB - Last synced at: 9 days ago - Pushed at: 17 days ago - Stars: 175 - Forks: 43

pthariensflame/agda-fumulas

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

Language: Agda - Size: 185 KB - Last synced at: 2 days ago - Pushed at: 19 days ago - Stars: 2 - Forks: 0

HoTT/HoTT-Agda

Development of homotopy type theory in Agda

Language: Agda - Size: 6.15 MB - Last synced at: 19 days ago - Pushed at: about 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: 4 days ago - Pushed at: over 4 years ago - Stars: 365 - Forks: 28

jespercockx/agda-core

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

Language: Agda - Size: 465 KB - Last synced at: 23 days ago - Pushed at: about 1 month ago - Stars: 48 - Forks: 3

freeman42x/blog

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

Size: 37.1 KB - Last synced at: 26 days ago - Pushed at: 26 days ago - Stars: 17 - Forks: 2

agda/agda-language-server

Language Server for Agda

Language: Haskell - Size: 390 KB - Last synced at: 8 days ago - Pushed at: 4 months ago - Stars: 107 - Forks: 15

smimram/fibred-polynomials

Formalizing polynomials in groupoids.

Language: Agda - Size: 63.5 KB - Last synced at: 16 days ago - Pushed at: about 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: 29 days ago - Pushed at: about 1 year ago - Stars: 41 - Forks: 12

ixaxaar/monoid.space

Learn pure math with agda :rocket:

Language: HTML - Size: 12.1 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 17 - Forks: 0

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: 26 days ago - Pushed at: about 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: about 1 year ago - Stars: 1 - Forks: 0

jonsterling/agda-calf

A cost-aware logical framework, embedded in Agda.

Language: Agda - Size: 10.2 MB - Last synced at: 22 days ago - Pushed at: 8 months ago - Stars: 61 - Forks: 2

xgrommx/agda-ecosystem

Size: 31.3 KB - Last synced at: 23 days ago - Pushed at: almost 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: about 1 month ago - Pushed at: about 2 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: 171 KB - Last synced at: 18 days ago - Pushed at: 18 days ago - Stars: 1 - 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: 9 days ago - Pushed at: 5 months ago - Stars: 33 - Forks: 7

konstantinosKokos/quill

🪶 Neural premise selection for Agda.

Language: Python - Size: 3.33 MB - Last synced at: about 2 months ago - Pushed at: 3 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: 9 days ago - Pushed at: about 2 years ago - Stars: 8 - Forks: 1

sourcedennis/docker-agda-mini

Small Docker images containing Agda

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

wenkokke/schmitty

Agda bindings to SMT-LIB2 compatible solvers.

Language: Agda - Size: 9.79 MB - Last synced at: about 2 months ago - Pushed at: 7 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: about 2 months ago - Pushed at: about 4 years ago - Stars: 6 - Forks: 0

alhassy/gentle-intro-to-reflection

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

Language: Agda - Size: 57.6 KB - Last synced at: 2 months ago - Pushed at: almost 3 years ago - Stars: 98 - Forks: 9

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: 3 days ago - Pushed at: over 2 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: about 1 month ago - Pushed at: over 8 years ago - Stars: 1 - Forks: 0

vendethiel/dependent-printf

I'm terrible at this, eh.

Language: Agda - Size: 109 KB - Last synced at: about 1 month ago - Pushed at: over 10 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: about 2 months ago - Pushed at: 2 months ago - Stars: 2 - Forks: 0

bracevac/dotter

Towards richer dependent types for DOT

Language: Coq - Size: 365 KB - Last synced at: 19 days ago - Pushed at: about 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: 7 days ago - Pushed at: almost 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: 14 days ago - Pushed at: about 3 years ago - Stars: 120 - Forks: 9

gallais/agdarsec

Total Parser Combinators in Agda

Language: Agda - Size: 9.95 MB - Last synced at: 8 days ago - Pushed at: almost 2 years ago - Stars: 126 - Forks: 11

smimram/agda-polygraphs

Polygraphs in Agda.

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

vikraman/2DTypes

Collaborative work on reversible computing

Language: TeX - Size: 42.3 MB - Last synced at: about 2 months ago - Pushed at: over 2 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: 11 months ago - Stars: 2 - Forks: 0

TOTBWF/cubical-categories

Category theory formalized in cubical agda

Language: Agda - Size: 37.1 KB - Last synced at: about 2 months ago - Pushed at: about 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: 16 days ago - Pushed at: over 6 years ago - Stars: 2 - Forks: 1

jonaprieto/agda-prop

A Library for Classical Propositional Logic in Agda

Language: Agda - Size: 442 KB - Last synced at: 16 days ago - Pushed at: over 5 years ago - Stars: 16 - Forks: 1

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: 4 months ago - Pushed at: 4 months ago - Stars: 3 - Forks: 0

leo-leesco/Computational-Logic-TD7

Sorting

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

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 months ago - Stars: 34 - Forks: 16

phijor/cubical-containers

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

cicada-lang/mugda

An implementation of the mugda paper

Language: TypeScript - Size: 2.99 MB - Last synced at: 28 days ago - Pushed at: 4 months ago - Stars: 2 - Forks: 2

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: 23 days ago - Pushed at: about 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: 20 days ago - Pushed at: over 3 years ago - Stars: 8 - Forks: 0

agda/agda-pkg

apkg - package manager for Agda

Language: Python - Size: 19 MB - Last synced at: 9 days ago - Pushed at: almost 4 years ago - Stars: 37 - Forks: 8

gergoerdi/stlc-agda

STLC-related snippets in Agda

Size: 164 KB - Last synced at: about 1 month ago - Pushed at: almost 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: 17 days ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 7

lemastero/agda-smash

smash product in Agda

Language: Agda - Size: 85.9 KB - Last synced at: 5 months ago - Pushed at: 5 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: 5 months ago - Pushed at: 5 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: about 2 months ago - Pushed at: 10 months ago - Stars: 0 - Forks: 0

jpvillaisaza/cain

Category theory applied to functional programming (undergraduate project)

Language: TeX - Size: 905 KB - Last synced at: 17 days ago - Pushed at: about 6 years ago - Stars: 32 - 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: 5 months ago - Pushed at: 5 months ago - Stars: 1 - Forks: 1

jpvillaisaza/abel

Category theory applied to functional programming

Language: Agda - Size: 80.1 KB - Last synced at: 17 days ago - Pushed at: over 8 years ago - Stars: 7 - 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: 14 days ago - Pushed at: over 3 years ago - Stars: 81 - Forks: 6

Seeker04/stlc-agda-elab

Agda formalisation of an elaborator for a simply typed language

Language: Agda - Size: 4.98 MB - Last synced at: about 2 months ago - Pushed at: 10 months 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: 6 months ago - Pushed at: 6 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: 6 months ago - Pushed at: 6 months ago - Stars: 3 - Forks: 0

algebraic-graphs/agda

The theory of algebraic graphs formalised in Agda

Language: Agda - Size: 42 KB - Last synced at: 5 months ago - Pushed at: almost 7 years ago - Stars: 87 - Forks: 6

martinescardo/HoTT-UF-Agda-Lecture-Notes

Lecture notes on univalent foundations of mathematics with Agda

Language: Agda - Size: 5.8 MB - Last synced at: 5 months ago - Pushed at: about 1 year ago - Stars: 219 - Forks: 18

choukh/agda-googology

formalized googology in agda

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

jespercockx/ataca

A TACtic library for Agda

Language: Agda - Size: 48.8 KB - Last synced at: 23 days ago - Pushed at: 7 months ago - Stars: 48 - Forks: 4

scott-fleischman/greek-grammar

Modeling Ancient Greek Grammar

Language: Agda - Size: 311 MB - Last synced at: 6 days ago - Pushed at: almost 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: 7 months ago - Pushed at: 7 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: 9 months ago - Pushed at: 9 months 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: 9 months ago - Pushed at: over 2 years ago - Stars: 22 - Forks: 1

andreasabel/agda2lagda

Simple conversion from Agda text to literate Agda text.

Language: Haskell - Size: 144 KB - Last synced at: 6 months ago - Pushed at: about 1 year ago - Stars: 14 - Forks: 0

fsestini/nbe-mltt-wes

Normalization by Evaluation for a version of Martin-Löf Type Theory with weak explicit substitutions.

Language: Agda - Size: 26.4 KB - Last synced at: 5 months ago - Pushed at: about 2 years ago - Stars: 6 - Forks: 0

choukh/agda-veblen

veblen function in agda

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

iwilare/formal-methods

Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language

Language: Agda - Size: 32.2 KB - Last synced at: 9 months ago - Pushed at: over 2 years ago - Stars: 14 - Forks: 1

PragmaTwice/TNT

some simple&naive formal proof of trivial Number Theory, using Agda/Coq, just to practice skills

Language: Agda - Size: 8.79 KB - Last synced at: 7 days ago - Pushed at: about 6 years ago - Stars: 8 - Forks: 1

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

Generated deloopings in Agda.

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

AJChapman/agda-frp

Functional Reactive Programming in Agda, adapting [Conal Elliott's Push-Pull Functional Reactive Programming](http://conal.net/papers/push-pull-frp/push-pull-frp.pdf).

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

kkd26/cam

Categorical Abstract Machine: Theory, Formalisation, Extensions

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

varikvalefor/mceliece

Language: Agda - Size: 1.35 MB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 0 - Forks: 0

iwilare/categorical-automata

Bicategories of automata, completeness of F-automata in monoidal categories, adjoints between (semi)bicategories; https://arxiv.org/pdf/2303.03867, https://arxiv.org/pdf/2303.03865, https://arxiv.org/abs/2305.00272

Language: Agda - Size: 578 KB - Last synced at: 9 months ago - Pushed at: 11 months ago - Stars: 15 - Forks: 1

yazaldefilimone/lambda-checker.agda

Language: Agda - Size: 1000 Bytes - Last synced at: 9 days ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

JonasHoefer/scoped-effects-agda

An implementation of scoped algebraic effects and handlers in Agda.

Language: TeX - Size: 13.7 MB - Last synced at: 9 months ago - Pushed at: about 4 years ago - Stars: 11 - Forks: 0

yitzchak/dicy 📦

A builder for LaTeX, knitr, literate Agda, literate Haskell and Pweave that automatically builds dependencies.

Language: TypeScript - Size: 2.23 MB - Last synced at: 3 days ago - Pushed at: about 6 years ago - Stars: 21 - Forks: 2

piotr-lewandowski/hoare-triples

Agda proof of soundness of Hoare Logic for a simple toy language

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

yitzchak/atom-dicy 📦

Compile LaTeX, knitr, literate Agda, literate Haskell and Pweave documents using DiCy from within Atom

Language: TypeScript - Size: 94.7 KB - Last synced at: 12 months ago - Pushed at: over 6 years ago - Stars: 2 - Forks: 0

Mari-W/System-Fo

formal proof of type preservation of the dictionary passing transform for system f

Language: Agda - Size: 13.1 MB - Last synced at: 12 months ago - Pushed at: about 2 years ago - Stars: 2 - Forks: 0

oisdk/agda-ring-solver 📦

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

Language: Agda - Size: 6.07 MB - Last synced at: 12 months ago - Pushed at: about 3 years ago - Stars: 38 - Forks: 4