Topic: "agda"
agda/agda
Agda is a dependently typed programming language / interactive theorem prover.
Language: Haskell - Size: 146 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 2,614 - Forks: 368
agda/agda-stdlib
The Agda standard library
Language: Agda - Size: 550 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 610 - Forks: 247
agda/cubical
An experimental library for Cubical Agda
Language: Agda - Size: 313 MB - Last synced at: 12 days ago - Pushed at: about 1 month ago - Stars: 477 - Forks: 145
HoTT/HoTT-Agda
Development of homotopy type theory in Agda
Language: Agda - Size: 6.15 MB - Last synced at: 21 days ago - Pushed at: about 6 years ago - Stars: 424 - Forks: 58
the1lab/1lab
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
Language: Agda - Size: 8.75 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 366 - Forks: 72
EgbertRijke/HoTT-Intro 📦
An introductory course to Homotopy Type Theory
Language: Agda - Size: 7.11 MB - Last synced at: 6 days ago - Pushed at: over 4 years ago - Stars: 365 - Forks: 28
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: 14 days ago - Pushed at: 14 days ago - Stars: 253 - Forks: 45
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
awesomo4000/awesome-provable
A curated set of links to formal methods involving provable code.
Size: 25.4 KB - Last synced at: 11 days ago - Pushed at: over 3 years ago - Stars: 202 - Forks: 10
banacorn/agda-mode-vscode
agda-mode on VS Code
Language: ReScript - Size: 4.77 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 175 - Forks: 44
agda/cornelis
agda-mode for neovim
Language: Haskell - Size: 12.1 MB - Last synced at: about 14 hours ago - Pushed at: 23 days ago - Stars: 150 - Forks: 24
copumpkin/categories
Categories parametrized by morphism equality, in Agda
Language: Agda - Size: 772 KB - Last synced at: about 1 year ago - Pushed at: over 5 years ago - Stars: 148 - Forks: 27
gallais/agdarsec
Total Parser Combinators in Agda
Language: Agda - Size: 9.95 MB - Last synced at: 10 days ago - Pushed at: almost 2 years ago - Stars: 126 - Forks: 11
ilya-klyuchnikov/ttlite
A SuperCompiler for Martin-Löf's Type Theory
Language: Scala - Size: 1.5 MB - Last synced at: 17 days ago - Pushed at: about 3 years ago - Stars: 120 - Forks: 9
HoTT-Intro/Agda
Agda formalisation of the Introduction to Homotopy Type Theory
Language: Agda - Size: 6.82 MB - Last synced at: over 1 year ago - Pushed at: over 3 years ago - Stars: 110 - Forks: 4
agda/agda-language-server
Language Server for Agda
Language: Haskell - Size: 390 KB - Last synced at: 10 days ago - Pushed at: 4 months ago - Stars: 107 - Forks: 15
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
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
vehicle-lang/vehicle
A toolkit for enforcing logical specifications on neural networks
Language: Haskell - Size: 23.9 MB - Last synced at: about 8 hours ago - Pushed at: about 9 hours ago - Stars: 88 - Forks: 9
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
scott-fleischman/agda-from-nothing
A workshop on learning Agda with minimal prerequisites.
Language: Agda - Size: 422 KB - Last synced at: 9 days ago - Pushed at: almost 9 years ago - Stars: 85 - Forks: 6
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: 17 days ago - Pushed at: over 3 years ago - Stars: 81 - Forks: 6
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: 28 days ago - Pushed at: about 3 years ago - Stars: 72 - Forks: 11
jonsterling/agda-calf
A cost-aware logical framework, embedded in Agda.
Language: Agda - Size: 10.2 MB - Last synced at: 24 days ago - Pushed at: 8 months ago - Stars: 61 - Forks: 2
banacorn/agda-mode 📦
agda-mode on Atom
Language: Reason - Size: 32.8 MB - Last synced at: about 1 year ago - Pushed at: about 4 years ago - Stars: 59 - Forks: 14
fredefox/cat
A formalization of category theory in cubical Agda
Language: Agda - Size: 3.96 MB - Last synced at: over 1 year ago - Pushed at: almost 5 years ago - Stars: 53 - Forks: 4
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: 25 days ago - Pushed at: about 7 years ago - Stars: 52 - Forks: 2
scott-fleischman/greek-grammar
Modeling Ancient Greek Grammar
Language: Agda - Size: 311 MB - Last synced at: 8 days ago - Pushed at: almost 7 years ago - Stars: 50 - Forks: 7
jespercockx/agda-core
A work-in-progress core language for Agda, in Agda
Language: Agda - Size: 465 KB - Last synced at: 25 days ago - Pushed at: about 1 month ago - Stars: 48 - Forks: 3
jespercockx/ataca
A TACtic library for Agda
Language: Agda - Size: 48.8 KB - Last synced at: 25 days ago - Pushed at: 7 months ago - Stars: 48 - Forks: 4
IntersectMBO/formal-ledger-specifications
Formal specifications of the cardano ledger
Language: Agda - Size: 193 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 41 - Forks: 16
isovector/certainty-by-construction
Source material for Certainty by Construction
Language: TeX - Size: 7.46 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 41 - Forks: 12
mr-ohman/logrel-mltt
A Logical Relation for Martin-Löf Type Theory in Agda
Language: Agda - Size: 4.2 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 40 - Forks: 10
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
wenkokke/AutoInAgda 📦
Proof automation – for Agda, in Agda.
Language: Agda - Size: 1.11 MB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 38 - Forks: 7
alhassy/AgdaCheatSheet
Basics of the dependently-typed functional language Agda ^_^
Language: Agda - Size: 460 KB - Last synced at: 6 months ago - Pushed at: over 3 years ago - Stars: 37 - Forks: 1
agda/agda-pkg
apkg - package manager for Agda
Language: Python - Size: 19 MB - Last synced at: 11 days ago - Pushed at: almost 4 years ago - Stars: 37 - Forks: 8
ice1k/ConsHoTT
Constructive Interpretations of HoTT
Language: TeX - Size: 148 KB - Last synced at: 12 months ago - Pushed at: over 4 years ago - Stars: 36 - Forks: 1
tree-sitter/tree-sitter-agda
Agda grammar for tree-sitter
Language: Yacc - Size: 31.1 MB - Last synced at: 7 days ago - Pushed at: 5 months ago - Stars: 34 - Forks: 16
ualib/agda-algebras
The Agda Universal Algebra Library (html docs available at the url below)
Language: Agda - Size: 65 MB - Last synced at: 11 days ago - Pushed at: 5 months ago - Stars: 33 - Forks: 7
gallais/agda-sizedIO
IO using sized types and copatterns
Language: Agda - Size: 4.56 MB - Last synced at: 28 days ago - Pushed at: about 4 years ago - Stars: 33 - Forks: 1
jpvillaisaza/cain
Category theory applied to functional programming (undergraduate project)
Language: TeX - Size: 905 KB - Last synced at: 19 days ago - Pushed at: about 6 years ago - Stars: 32 - Forks: 0
gallais/agda-presburger
Deciding Presburger arithmetic in agda
Language: Agda - Size: 155 KB - Last synced at: 28 days ago - Pushed at: about 2 years ago - Stars: 31 - Forks: 3
frex-project/agda-fragment
Algebraic proof discovery in Agda
Language: Agda - Size: 2.39 MB - Last synced at: 12 months ago - Pushed at: over 3 years ago - Stars: 31 - Forks: 2
xgrommx/agda-ecosystem
Size: 31.3 KB - Last synced at: 25 days ago - Pushed at: almost 7 years ago - Stars: 30 - Forks: 1
L-TChen/MtacAR
Mtac in Agda
Language: Agda - Size: 98.6 KB - Last synced at: 16 days ago - Pushed at: almost 4 years ago - Stars: 28 - Forks: 0
divipp/frp_agda 📦
Functional Reactive Programming with Agda
Size: 51.8 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 26 - Forks: 1
ice1000/agda-mode
Accessing Agda's interaction mode via command line & external tactic for Agda.
Language: Rust - Size: 225 KB - Last synced at: 6 days ago - Pushed at: over 4 years ago - Stars: 26 - Forks: 4
effectfully/inference-in-agda
A tutorial on how Agda infers things
Language: HTML - Size: 1.17 MB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 25 - Forks: 0
lclem/agda-kernel
An experimental Agda kernel for Jupyter
Language: Jupyter Notebook - Size: 19.9 MB - Last synced at: about 1 month ago - Pushed at: about 3 years ago - Stars: 24 - Forks: 2
wenkokke/msla2014
wherein I implement several substructural logics in Agda
Language: Agda - Size: 2.04 MB - Last synced at: about 2 months ago - Pushed at: over 6 years ago - Stars: 24 - Forks: 2
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
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: about 7 hours ago - Pushed at: about 6 years ago - Stars: 21 - Forks: 2
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
ualib/ualib.github.io
The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) that formalizes the foundations of universal algebra in dependent type theory using the Agda proof assistant language.
Language: TeX - Size: 52.7 MB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 19 - Forks: 2
marcinjangrzybowski/cubeViz2
Language: Haskell - Size: 6.66 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 18 - Forks: 2
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
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: 19 days ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 7
freeman42x/blog
Software engineering and artificial general intelligence blog of Răzvan Flavius Panda
Size: 37.1 KB - Last synced at: 28 days ago - Pushed at: 28 days ago - Stars: 17 - Forks: 2
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
jmlowenthal/agda-c
Verified C programming in Agda
Language: Agda - Size: 273 KB - Last synced at: about 1 year ago - Pushed at: about 4 years ago - Stars: 16 - Forks: 1
jonaprieto/agda-prop
A Library for Classical Propositional Logic in Agda
Language: Agda - Size: 442 KB - Last synced at: 19 days ago - Pushed at: over 5 years ago - Stars: 16 - Forks: 1
gergoerdi/universe-of-syntax
A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.
Language: Agda - Size: 38.1 KB - Last synced at: about 1 month ago - Pushed at: over 7 years ago - Stars: 16 - Forks: 0
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
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
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
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
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
superhaNds/cwfs
Formalization of Categories with Families
Language: Agda - Size: 1.45 MB - Last synced at: over 1 year ago - Pushed at: over 3 years ago - Stars: 13 - Forks: 0
banacorn/language-agda 📦
Agda language support for the Atom editor
Size: 41 KB - Last synced at: about 1 year ago - Pushed at: over 4 years ago - Stars: 13 - Forks: 5
scott-fleischman/agda-from-nothing-2017
Agda from Nothing: Order in the Types
Language: Agda - Size: 553 KB - Last synced at: 9 days ago - Pushed at: about 8 years ago - Stars: 13 - Forks: 0
agda/package-index
A package Index for agda libraries
Size: 57.6 KB - Last synced at: about 1 year ago - Pushed at: about 4 years ago - Stars: 12 - Forks: 2
metaborg/mj.agda
https://metaborg.github.io/mj.agda/
Language: Agda - Size: 1.91 MB - Last synced at: about 1 year ago - Pushed at: over 4 years ago - Stars: 12 - Forks: 1
felko/linear-algebra
Linear algebra formalization in Agda
Language: Agda - Size: 499 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 12 - Forks: 0
L-TChen/FiniteSets
Fintie Sets in Cubical Agda
Language: Agda - Size: 69.3 KB - Last synced at: 19 days ago - Pushed at: over 5 years ago - Stars: 12 - Forks: 0
fsestini/tt-in-cubical
Type Theory in Type Theory using Cubical Agda
Language: Agda - Size: 70.3 KB - Last synced at: 5 months ago - Pushed at: about 6 years ago - Stars: 12 - Forks: 0
alan-j-hu/camyll
Static site generator
Language: OCaml - Size: 208 KB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 11 - Forks: 1
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
ice1k/Theorems
:globe_with_meridians: Theorems that rule this multiverse
Language: Agda - Size: 76.2 KB - Last synced at: 5 months ago - Pushed at: over 6 years ago - Stars: 11 - Forks: 2
ernius/mergesort
Merge sort correctness proof
Language: Agda - Size: 800 KB - Last synced at: over 1 year ago - Pushed at: almost 10 years ago - Stars: 10 - Forks: 0
ncfavier/cubical-experiments
Experiments with Cubical Agda
Language: Agda - Size: 163 KB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 9 - Forks: 1
juniorxxue/contextual-typing
Contextual Typing, formalized in Agda
Language: Agda - Size: 3.64 MB - Last synced at: 5 days ago - Pushed at: 2 months ago - Stars: 9 - Forks: 0
felipeperet/logic Fork of rodrigogribeiro/logic
An adventure on formalizing logics using the Agda programming language
Language: Agda - Size: 57.6 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 9 - Forks: 2
quchen/agda-learning
Stuff I’m writing to learn Agda.
Language: Agda - Size: 73.2 KB - Last synced at: about 1 month ago - Pushed at: almost 5 years ago - Stars: 9 - Forks: 0
joom/modal
Compilation of modal logic based functional language ML5 to JavaScript.
Language: Agda - Size: 106 KB - Last synced at: 18 days ago - Pushed at: about 8 years ago - Stars: 9 - Forks: 1
andreasabel/agda-automata
Formalisation of automata in Agda
Language: Agda - Size: 218 KB - Last synced at: 2 months ago - Pushed at: about 1 year ago - Stars: 8 - Forks: 0
fsestini/nbe-weak-stlc
Agda formalization of normalization by evaluation for the confluent simply-typed weak lambda-calculus.
Language: Agda - Size: 29.3 KB - Last synced at: 5 months ago - Pushed at: about 2 years ago - Stars: 8 - Forks: 0
smimram/fibred-polynomials
Formalizing polynomials in groupoids.
Language: Agda - Size: 63.5 KB - Last synced at: 18 days ago - Pushed at: about 2 years ago - Stars: 8 - Forks: 1
wolverian/agda-template
A template for an Agda project with automatic GitHub Pages support
Language: CSS - Size: 2.44 MB - Last synced at: 12 days ago - Pushed at: about 2 years ago - Stars: 8 - Forks: 1
gitpod-samples/template-agda
An Agda template, configured for Gitpod (www.gitpod.io) to give you pre-built, ephemeral development environments in the cloud.
Language: Agda - Size: 4.88 KB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 8 - Forks: 1
akiomik/plfa-solutions
Solutions for PLFA (Programming Language Foundations in Agda) exercise
Language: Agda - Size: 122 KB - Last synced at: 22 days ago - Pushed at: over 3 years ago - Stars: 8 - Forks: 0
doofin/hott-examples
Homotopy type theory for theorem proving with univalence
Language: Agda - Size: 1.47 MB - Last synced at: 5 days ago - Pushed at: over 3 years ago - Stars: 8 - Forks: 0
jmlowenthal/staged-streams.agda
An implementation of the staged Strymonas streams library in Agda for C
Language: Haskell - Size: 309 KB - Last synced at: about 1 year ago - Pushed at: almost 5 years ago - Stars: 8 - 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: 9 days ago - Pushed at: about 6 years ago - Stars: 8 - Forks: 1
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: 13 days ago - Pushed at: 13 days ago - Stars: 7 - Forks: 5
Lolirofle/stuff-in-agda
Formal proofs in mathematics/computer science/logic formalized in the Agda language. A hobby project I am working on in my free time.
Language: Agda - Size: 4.67 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 7 - Forks: 1
wenkokke/amethyst
Agda library for verifying neural networks.
Language: Agda - Size: 4.62 MB - Last synced at: about 2 months ago - Pushed at: over 4 years ago - Stars: 7 - Forks: 0
desi-ivanov/agda-regexp-automata
Formalization of Regular Languages in Agda: regular expressions, finite-state automata, proof of equivalence, proof of the pumping lemma.
Language: Agda - Size: 840 KB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 7 - Forks: 0
scott-fleischman/agda-travis
Example repo for building Agda files with Travis CI
Language: Agda - Size: 10.7 KB - Last synced at: 8 days ago - Pushed at: over 6 years ago - Stars: 7 - Forks: 1
SuprDewd/agda-translation-method
An Agda library for turning equations into bijections using the translation method
Language: Agda - Size: 6.41 MB - Last synced at: about 1 year ago - Pushed at: almost 8 years ago - Stars: 7 - Forks: 0
